Terence Tao
@teorth.bsky.social
Mathematician at UCLA. My primary social media account is https://mathstodon.xyz/@tao . I also have a blog at https://terrytao.wordpress.com/ and a home page at https://www.math.ucla.edu/~tao/
Tanya Klowden and I have uploaded a further sample chapter to our "cosmic distance ladder" book: terrytao.wordpress.com/books/climbi... . See also the blog post terrytao.wordpress.com/2025/11/21/c...
Climbing the cosmic distance ladder
Climbing the cosmic distance ladder Tanya Klowden and Terence Tao in preparation This project is based on a public lecture on the cosmic distance ladder that I have given on occasion. Working with …
terrytao.wordpress.com
November 22, 2025 at 12:39 AM
Tanya Klowden and I have uploaded a further sample chapter to our "cosmic distance ladder" book: terrytao.wordpress.com/books/climbi... . See also the blog post terrytao.wordpress.com/2025/11/21/c...
A new paper with Bogdan Georgiev, Javier Gomez-Serrano, and Adam Zsolt Wagner: "Mathematical exploration and discovery at scale" arxiv.org/abs/2511.02864. Further discussion is at terrytao.wordpress.com/2025/11/05/m...
Mathematical exploration and discovery at scale
AlphaEvolve is a generic evolutionary coding agent that combines the generative capabilities of LLMs with automated evaluation in an iterative evolutionary framework that proposes, tests, and refines ...
arxiv.org
November 6, 2025 at 3:42 AM
A new paper with Bogdan Georgiev, Javier Gomez-Serrano, and Adam Zsolt Wagner: "Mathematical exploration and discovery at scale" arxiv.org/abs/2511.02864. Further discussion is at terrytao.wordpress.com/2025/11/05/m...
Reposted by Terence Tao
Calling Bay Area math enthusiasts interested in weekly sessions doing rigorous foundational mathematics the modern way - with computer-verified proofs in Lean.
(An experiment in rigorous math education outside traditional academia)
(An experiment in rigorous math education outside traditional academia)
September 24, 2025 at 5:05 AM
Calling Bay Area math enthusiasts interested in weekly sessions doing rigorous foundational mathematics the modern way - with computer-verified proofs in Lean.
(An experiment in rigorous math education outside traditional academia)
(An experiment in rigorous math education outside traditional academia)
I started a crowdsourced meta-project to list all the other crowdsourced mathematical research projects that are currently active and seeking participants: mathoverflow.net/questions/50...
List of crowdsourced math projects actively seeking participants
I believe that with the advent of modern online collaboration platforms (such as Github), proof assistant languages (such as Lean), and (potentially) AI tools, there are many emerging opportunities...
mathoverflow.net
September 23, 2025 at 4:08 PM
I started a crowdsourced meta-project to list all the other crowdsourced mathematical research projects that are currently active and seeking participants: mathoverflow.net/questions/50...
A first proof-of-concept outcome for the erdosproblems.com - OEIS linkage project: with a useful assist from AI, the OEIS was used to locate a proof in the literature for an Erdos problem that was previously marked as "open". mathstodon.xyz/deck/@tao/11...
Terence Tao (@[email protected])
Here is a first proof-of-concept demonstration of an actual outcome for the erdosproblems/OEIS linkage project. There are a number of Erdos problems relating to irrationality of specific series. I ask...
mathstodon.xyz
September 2, 2025 at 4:27 PM
A first proof-of-concept outcome for the erdosproblems.com - OEIS linkage project: with a useful assist from AI, the OEIS was used to locate a proof in the literature for an Erdos problem that was previously marked as "open". mathstodon.xyz/deck/@tao/11...
Thomas Bloom and I are launching a crowdsourced project to link up Thomas's erdosproblems.com site with the #OEIS, by systematically calculating the various integer sequences associated with the Erdos problems and crosschecking them against the OEIS database: terrytao.wordpress.com/2025/08/31/a...
Erdős Problems
erdosproblems.com
September 1, 2025 at 7:31 AM
Thomas Bloom and I are launching a crowdsourced project to link up Thomas's erdosproblems.com site with the #OEIS, by systematically calculating the various integer sequences associated with the Erdos problems and crosschecking them against the OEIS database: terrytao.wordpress.com/2025/08/31/a...
Reposted by Terence Tao
SLMath (MSRI) announces three new research initiatives in Berkeley, California: Call for Proposals for AxIOM month-long programs to begin in Spring 2027, and applications for Summer 2026 PROOF and LATTICE independent research groups. Learn more at www.slmath.org/news-and-eve....
August 29, 2025 at 4:40 PM
SLMath (MSRI) announces three new research initiatives in Berkeley, California: Call for Proposals for AxIOM month-long programs to begin in Spring 2027, and applications for Summer 2026 PROOF and LATTICE independent research groups. Learn more at www.slmath.org/news-and-eve....
I wrote an op-ed on the world-class STEM research ecosystem in the United States, and how this ecosystem is now under attack on multiple fronts by the current administration: newsletter.ofthebrave.org/p/im-an-awar...
I’m an award-winning mathematician. Trump just cut my funding.
The “Mozart of Math” tried to stay out of politics. Then it came for his research.
newsletter.ofthebrave.org
August 18, 2025 at 3:45 PM
I wrote an op-ed on the world-class STEM research ecosystem in the United States, and how this ecosystem is now under attack on multiple fronts by the current administration: newsletter.ofthebrave.org/p/im-an-awar...
#IPAM (the institute for pure and applied mathematics) is facing a critical shortfall for operating expenses due to an unexpected suspension of NSF funding www.ipam.ucla.edu/news/nsf-fun... . Donations for emergency continuity of operations funding can be made at
giving.ucla.edu/Campaign/Donat
giving.ucla.edu/Campaign/Donat
www.ipam.ucla.edu
August 8, 2025 at 12:48 AM
#IPAM (the institute for pure and applied mathematics) is facing a critical shortfall for operating expenses due to an unexpected suspension of NSF funding www.ipam.ucla.edu/news/nsf-fun... . Donations for emergency continuity of operations funding can be made at
giving.ucla.edu/Campaign/Donat
giving.ucla.edu/Campaign/Donat
My thoughts on the crucial importance of methodology on self-reported AI performance on mathematics competitions, and my policy on commenting on such reports going forward: mathstodon.xyz/@tao/1148814...
Terence Tao (@[email protected])
It is tempting to view the capability of current AI technology as a singular quantity: either a given task X is within the ability of current tools, or it is not. However, there is in fact a very wid...
mathstodon.xyz
July 19, 2025 at 10:37 PM
My thoughts on the crucial importance of methodology on self-reported AI performance on mathematics competitions, and my policy on commenting on such reports going forward: mathstodon.xyz/@tao/1148814...
The #SalemPrize for 2025 is now accepting nominations until September 15th. www.ias.edu/math/activit... (I am the chair of the Scientific Committee for the prize.) A bit more information in my blog post on this: terrytao.wordpress.com/2025/07/08/s...
Salem Prize
About
www.ias.edu
July 8, 2025 at 3:44 PM
The #SalemPrize for 2025 is now accepting nominations until September 15th. www.ias.edu/math/activit... (I am the chair of the Scientific Committee for the prize.) A bit more information in my blog post on this: terrytao.wordpress.com/2025/07/08/s...
A new #CosmicDistanceLadder post to mark the summer solstice, on how astronomical measurements, from the time of Eratosthenes to the modern day, rely on the tireless (and often unsung) efforts of many careful and precise data collectors. www.instagram.com/p/DLG6a_WIWyb
June 20, 2025 at 4:18 AM
A new #CosmicDistanceLadder post to mark the summer solstice, on how astronomical measurements, from the time of Eratosthenes to the modern day, rely on the tireless (and often unsung) efforts of many careful and precise data collectors. www.instagram.com/p/DLG6a_WIWyb
I have just launched a "Lean companion" to my textbook "Analysis I": github.com/teorth/estim... . This gives a Lean translation (or paraphrasing) of the various definitions, theorems, and exercises in the textbook into Lean.
Further discussion at terrytao.wordpress.com/2025/05/31/a...
Further discussion at terrytao.wordpress.com/2025/05/31/a...
github.com
May 31, 2025 at 5:32 PM
I have just launched a "Lean companion" to my textbook "Analysis I": github.com/teorth/estim... . This gives a Lean translation (or paraphrasing) of the various definitions, theorems, and exercises in the textbook into Lean.
Further discussion at terrytao.wordpress.com/2025/05/31/a...
Further discussion at terrytao.wordpress.com/2025/05/31/a...
A video on an actual formalization task from my Polynomial Freiman Ruzsa (PFR) project, which is sufficiently tricky (and sufficiently far from existing training data of current models) that one still has to largely formalize these proofs by "hand": www.youtube.com/watch?v=6uLX...
Formalizing a proof in Lean by hand
YouTube video by Terence Tao
www.youtube.com
May 26, 2025 at 12:10 AM
A video on an actual formalization task from my Polynomial Freiman Ruzsa (PFR) project, which is sufficiently tricky (and sufficiently far from existing training data of current models) that one still has to largely formalize these proofs by "hand": www.youtube.com/watch?v=6uLX...
A new #CosmicDistanceLadder post on how the distance ladder can also be used to measure cosmic durations, as well as cosmic distances. www.instagram.com/p/DJ2ra2soG4j
May 20, 2025 at 12:00 AM
A new #CosmicDistanceLadder post on how the distance ladder can also be used to measure cosmic durations, as well as cosmic distances. www.instagram.com/p/DJ2ra2soG4j
A third video in my occasional series on #Lean4 formalization workflows, this time focusing on how relying extensively on #GitHubCopilot fares against standard "epsilon delta" type problems in analysis. www.youtube.com/watch?v=c1ix...
Formalizing a proof in Lean using Github Copilot only
YouTube video by Terence Tao
www.youtube.com
May 17, 2025 at 9:46 PM
A third video in my occasional series on #Lean4 formalization workflows, this time focusing on how relying extensively on #GitHubCopilot fares against standard "epsilon delta" type problems in analysis. www.youtube.com/watch?v=c1ix...
A followup to my previous video, in which I now see how #Claude and #o4mini do at formalizing a slightly different proof of the same algebraic implication, after being given the initial informal and formal proofs as reference. www.youtube.com/watch?v=zZr5...
Formalizing a proof in Lean using Claude and o4
YouTube video by Terence Tao
www.youtube.com
May 13, 2025 at 5:40 AM
A followup to my previous video, in which I now see how #Claude and #o4mini do at formalizing a slightly different proof of the same algebraic implication, after being given the initial informal and formal proofs as reference. www.youtube.com/watch?v=zZr5...
As an experiment, I tried to use automated tools to formalize (in as "mindless" a fashion as possible) a one-page human written proof into Lean. You can watch the results here: www.youtube.com/watch?v=cyyR...
Formalizing a proof in Lean using Github copilot and canonical
YouTube video by Terence Tao
www.youtube.com
May 11, 2025 at 1:16 AM
As an experiment, I tried to use automated tools to formalize (in as "mindless" a fashion as possible) a one-page human written proof into Lean. You can watch the results here: www.youtube.com/watch?v=cyyR...
DARPA's "Exponentiating mathematics" (expMath) program, which is launching a challenge to develop and evaluate "AI collaborators" for assist in decomposing and formalizing informal mathematical proofs, is now taking short abstract proposal submissions: sam.gov/opp/869c8d73...
SAM.gov
sam.gov
May 1, 2025 at 5:36 PM
DARPA's "Exponentiating mathematics" (expMath) program, which is launching a challenge to develop and evaluate "AI collaborators" for assist in decomposing and formalizing informal mathematical proofs, is now taking short abstract proposal submissions: sam.gov/opp/869c8d73...
After 200 days, we finally have 100% completion on the primary goal of the Equational Theories Project to formally resolve >22 million implications between 4694 equational laws, using modern proof assistants, collaboration platforms, and automated theorem provers. teorth.github.io/equational_t...
April 14, 2025 at 5:06 PM
After 200 days, we finally have 100% completion on the primary goal of the Equational Theories Project to formally resolve >22 million implications between 4694 equational laws, using modern proof assistants, collaboration platforms, and automated theorem provers. teorth.github.io/equational_t...
A new #CosmicDistanceLadder post, on intriguing hints from the DESI survey data that suggests that the cosmological constant (aka "dark energy) might not, in fact, be constant after all. www.instagram.com/p/DIP0yy5oDUu
April 10, 2025 at 4:00 AM
A new #CosmicDistanceLadder post, on intriguing hints from the DESI survey data that suggests that the cosmological constant (aka "dark energy) might not, in fact, be constant after all. www.instagram.com/p/DIP0yy5oDUu
A new #CosmicDistanceLadder post on why lunar and solar eclipses tend to come in pairs (for instance, the solar eclipse next week is paired with the lunar eclipse from last week). www.instagram.com/p/DHkS3EcA40L
March 24, 2025 at 4:42 AM
A new #CosmicDistanceLadder post on why lunar and solar eclipses tend to come in pairs (for instance, the solar eclipse next week is paired with the lunar eclipse from last week). www.instagram.com/p/DHkS3EcA40L
Reposted by Terence Tao
Cosmic Distance Calibration xkcd.com/3066
March 21, 2025 at 7:49 PM
Cosmic Distance Calibration xkcd.com/3066
A new #CosmicDistanceLadder post, on how the recent lunar eclipse from the vantage point of the Earth becomes a solar eclipse from the vantage point of the Moon: www.instagram.com/p/DHR1tuWonDR/
March 17, 2025 at 1:50 AM
A new #CosmicDistanceLadder post, on how the recent lunar eclipse from the vantage point of the Earth becomes a solar eclipse from the vantage point of the Moon: www.instagram.com/p/DHR1tuWonDR/
Lunar eclipses, such as the one yesterday, were one of the earliest pieces of scientific evidence that the Earth was basically a round sphere, already known to Aristotle: regardless of the position of the eclipse in the light sky, the shadow of the Earth on the Moon was always circular.
March 14, 2025 at 9:51 PM
Lunar eclipses, such as the one yesterday, were one of the earliest pieces of scientific evidence that the Earth was basically a round sphere, already known to Aristotle: regardless of the position of the eclipse in the light sky, the shadow of the Earth on the Moon was always circular.