I should really know better than to say something like that for a figure as revered as Terry Tao, but, he has taken OpenAI's money to shoot an advert for them [1] and, sorry but I can't believe he is entirely unbiased; or very unbiased for that.
Terry Tao is a next level vibe coder: he inspires people to do his vibe coding for him. As someone with a background in advanced math, though never even close to Tao's level, I find myself skeptical about this type of mathematics. I don't personally find it beautiful and it feels like the line between the profound and the trivial (as in of minimal importance not difficulty) is blurry. One could argue for pure mathematics that is of no practical utility but is aesthetically beautiful, but I struggle to see the beauty in a gargantuan lean proof constructed by 100 different people. Perhaps this work will lead to deeper insight about the universe and the human condition, but I catch a whiff of problem solving for the sake of problem solving untethered from a deeper sense of purpose and meaning.
Much (most?) of math consists in transmission of it (according to Thurston [1]), a 1000-page proof with no possibility of transmission is mostly useless. The proof of Fermat's last Theorem is important in itself, and adds much more than the mere result.
I am not talking about the supposed "beauty" of a proof (I do not believe in that concept, rather in "elegance", which is not the same), I am talking about the proof itself, and the insights it provides.
Outside of some niche specializations like cryptography, math isn't practiced because of "consequences". Most mathematicians take pride in their work not having any obvious practical applications. They're also overwhelmingly working in university settings where they're not expected to generate revenue or deliver practical results.
We basically subsidize the practice of mathematics as an art form, and if you try to take the artistry away, you might find that the artists don't want to play along. And I guess you can imagine future robo-math production lines without any human involvement, and then LLMs finding applications for the resulting theorems, but it's not possible today.
You put it perfectly. And all these AI math startups don't actually care about mathematics. They are just using it as a proxy for general reasoning, with the VC pitch being some kind of world domination after they crack these problems.
At the universities I’ve been to (as a student and now faculty), «applied mathematics» and «statistics» have been the two largest divisions. But perhaps that’s a bias from engineering-heavy universities?
Why prove the Pythagorean theorem rather than just prove 3^2 + 4^2 = 5^2?
For any practical application, you are only interested in finite set of concrete identities, so anything beyond that is surplus to requirements, surely?
> For any practical application, you are only interested in finite set of concrete identities
I do a lot of numerical work in settings where computational efficiency is useful.
In my work, most cases you can do numerically using integration or Monte Carlo sampling or whatever.
It’s slow. It often pays to find a closed-form solution. Even if it’s just a starting point that needs refinement.
To put in terms of the Pythagorean theorem: Proving the Pythagorean theorem gives you a relationship that’s reliable, fast to evaluate, and general. Proving individual tuples gives you none of this.
That doesn’t even touch on how theorems give us a glimpse at deeper structure and truths. Proving a bunch of right-triangle tuples will probably never lead you to the rest of the identities in trig.
I think you may be interested in more abstract things. In this case, let's say you're creating a program for a 3D printed thing, and you have to fit a diagonal cardboard in a rectangular box, you'd like to be sure that the Pythagorean theorem holds even in cases where you haven't tried it out.
Arguments about beauty don't lead anywhere constructive because they are too observer- and context-dependent. Poincaré himself was decrying continuous non-differentiable functions as abominations. The monster group is, well, just like that. What feels intellectually ugly for one generation is natural for the next, and the field moves on
That's not what op is arguing. To use your example, coming up with singular examples of continuous non-differentiable functions is an example of "ugly" mathematics, whereas putting them into a nice framework where they can be analyzed as a whole (i.e. functional analysis, density of such functions, etc...) is an example "elegant and insightful" mathematics. The same with the monster group, on its own maybe nothing special, but then you have the connections with other branches of math. Tao seems so focused on the individual problems and not their connections/generalizations.
Well one does have to come up with continuous non-differentiable functions to begin with, right? Weierstrass had to shock the community with his weird series that's almost everywhere nondifferentiable before people could conceive of a nice framework that includes them. People do not invent whole encompassing abstractions out of nowhere
> Arguments about beauty don't lead anywhere constructive because they are too observer- and context-dependent.
Meh. You can successfully argue that there is no objective anything. It's all just our perception and the emotions we associate with it. We built entire civilizations on subjective notions of good, evil, beauty, and so on. So where do you draw the line between "acceptably subjective" and "too subjective"? And are you sure it's not just a subjective code name for "the thing I don't like"?
Ultimately, people practice mathematics mostly for abstract reasons. It's not a field where you routinely ship products and get rich by meeting market demand. If 99% of contemporary mathematicians don't want to become prompt engineers, there's nothing that makes the transition to AI math inevitable. If not mathematicians, the only party with vested interest in that would be the PR departments of frontier labs.
Agreed, mathematics is ugly without ai. I feel beauty is in massive complexity and intricacy. Every time I see a small proof it feels too easy and trivial. Triviality and simplicity is ugly to me.
I think what people find beautiful in math is largely something that enables the mathematics (or physics) to be translated to something that they can think about intuitively, and what people can handle in an intuitive way is largely an artifact of what the brain evolved to be able to think about "naturally". But it's quite possible that most things that are true about the universe or math are just ugly and unintuitive, and the pursuit of truth shouldn't necessarily be limited by what people can easily reason about and hold in their heads.
Beautiful explanations are lovely when they exist, but we shouldn't wait for them if we can also find the truth through an ugly method.
Quantamagazine is essentially Renaissance Fund, which is heavily invested in AI.
This is a clever piece reminding people of Tao's pre-AI Lean efforts. Now, however, Tao and especially Gowers are receiving AI money and have AI positions so they are far from unbiased.
Or maybe they have caught Feynman's "computer disease"? Either way, this is a hype piece.
Ahem. Define "Pre-AI". Automated theorem proving has been an AI task right from the very beginning with Simon and Newell's Logic Theorist, presented at the Dartmouth workshop in 1956.
Logic Theorist soon proved 38 of the first 52 theorems in chapter 2 of the Principia Mathematica. The proof of theorem 2.85 was actually more elegant than the proof produced laboriously by hand by Russell and Whitehead (2026-03-20: What is called here Theorem 2.85 is, in fact, numbered as 2.53 in the page 107 of the 1963 Cambridge University Press edition (https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_M...) and which appears, under the same 2.53 number, on page 112 of the 1910 CUP Edition, according to the digitalization on wikibooks (https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Pri...)). Simon was able to show the new proof to Russell himself who "responded with delight".[17] They attempted to publish the new proof in The Journal of Symbolic Logic, but it was rejected on the grounds that a new proof of an elementary mathematical theorem was not notable, apparently overlooking the fact that one of the authors was a computer program.[18][17]
Maybe some people only understand "AI" to mean "LLMs" but, particularly in maths, LLMs ain't going nowhere without a symbolic solver (or a human mathematician) verifying their output.
> Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness.
mathlib and lean are currently too cumbersome for many researchers to use in say algebraic geometry, but maybe more suitable for combinatorics where it has been applied recently.
I should really know better than to say something like that for a figure as revered as Terry Tao, but, he has taken OpenAI's money to shoot an advert for them [1] and, sorry but I can't believe he is entirely unbiased; or very unbiased for that.
_____________________
[1] https://youtu.be/cdflu9ZXZGE?si=f1xi65r7kZM8s1JI
I do not know about this but, to be honest, he (or his Dpt, or whatever) has the money and connections to try the hidden-behind-closed-doors stuff.
We mere mortals (I am a prof. of Maths at Uni) do not.
Terry Tao is a next level vibe coder: he inspires people to do his vibe coding for him. As someone with a background in advanced math, though never even close to Tao's level, I find myself skeptical about this type of mathematics. I don't personally find it beautiful and it feels like the line between the profound and the trivial (as in of minimal importance not difficulty) is blurry. One could argue for pure mathematics that is of no practical utility but is aesthetically beautiful, but I struggle to see the beauty in a gargantuan lean proof constructed by 100 different people. Perhaps this work will lead to deeper insight about the universe and the human condition, but I catch a whiff of problem solving for the sake of problem solving untethered from a deeper sense of purpose and meaning.
> I struggle to see the beauty in a gargantuan lean proof constructed by 100 different people
Why does it need to be beautiful? Once you proved it it's true and you can use its consequences in math, sciences and engineerings.
Much (most?) of math consists in transmission of it (according to Thurston [1]), a 1000-page proof with no possibility of transmission is mostly useless. The proof of Fermat's last Theorem is important in itself, and adds much more than the mere result.
I am not talking about the supposed "beauty" of a proof (I do not believe in that concept, rather in "elegance", which is not the same), I am talking about the proof itself, and the insights it provides.
[1] https://www.ams.org/journals/bull/1994-30-02/S0273-0979-1994...
What is the difference between "beauty" and "elegance" of a proof?
Outside of some niche specializations like cryptography, math isn't practiced because of "consequences". Most mathematicians take pride in their work not having any obvious practical applications. They're also overwhelmingly working in university settings where they're not expected to generate revenue or deliver practical results.
We basically subsidize the practice of mathematics as an art form, and if you try to take the artistry away, you might find that the artists don't want to play along. And I guess you can imagine future robo-math production lines without any human involvement, and then LLMs finding applications for the resulting theorems, but it's not possible today.
You put it perfectly. And all these AI math startups don't actually care about mathematics. They are just using it as a proxy for general reasoning, with the VC pitch being some kind of world domination after they crack these problems.
Are you sure that’s «most» mathematicians?
At the universities I’ve been to (as a student and now faculty), «applied mathematics» and «statistics» have been the two largest divisions. But perhaps that’s a bias from engineering-heavy universities?
> Why does it need to be beautiful?
“Beauty will save the world”
Why prove the Pythagorean theorem rather than just prove 3^2 + 4^2 = 5^2?
For any practical application, you are only interested in finite set of concrete identities, so anything beyond that is surplus to requirements, surely?
> For any practical application, you are only interested in finite set of concrete identities
I do a lot of numerical work in settings where computational efficiency is useful.
In my work, most cases you can do numerically using integration or Monte Carlo sampling or whatever.
It’s slow. It often pays to find a closed-form solution. Even if it’s just a starting point that needs refinement.
To put in terms of the Pythagorean theorem: Proving the Pythagorean theorem gives you a relationship that’s reliable, fast to evaluate, and general. Proving individual tuples gives you none of this.
That doesn’t even touch on how theorems give us a glimpse at deeper structure and truths. Proving a bunch of right-triangle tuples will probably never lead you to the rest of the identities in trig.
I think you may be interested in more abstract things. In this case, let's say you're creating a program for a 3D printed thing, and you have to fit a diagonal cardboard in a rectangular box, you'd like to be sure that the Pythagorean theorem holds even in cases where you haven't tried it out.
Arguments about beauty don't lead anywhere constructive because they are too observer- and context-dependent. Poincaré himself was decrying continuous non-differentiable functions as abominations. The monster group is, well, just like that. What feels intellectually ugly for one generation is natural for the next, and the field moves on
That's not what op is arguing. To use your example, coming up with singular examples of continuous non-differentiable functions is an example of "ugly" mathematics, whereas putting them into a nice framework where they can be analyzed as a whole (i.e. functional analysis, density of such functions, etc...) is an example "elegant and insightful" mathematics. The same with the monster group, on its own maybe nothing special, but then you have the connections with other branches of math. Tao seems so focused on the individual problems and not their connections/generalizations.
Well one does have to come up with continuous non-differentiable functions to begin with, right? Weierstrass had to shock the community with his weird series that's almost everywhere nondifferentiable before people could conceive of a nice framework that includes them. People do not invent whole encompassing abstractions out of nowhere
Great point, I think the argument you could make about Tao (fairly or unfairly) is he never tries to build that framework.
According to legends Pythagoreans tried to surpress existence of irrational numbers because they couldn't be expressed as ratio of natural numbers
Supposedly even drowned their member that divulged their existence.
> Arguments about beauty don't lead anywhere constructive because they are too observer- and context-dependent.
Meh. You can successfully argue that there is no objective anything. It's all just our perception and the emotions we associate with it. We built entire civilizations on subjective notions of good, evil, beauty, and so on. So where do you draw the line between "acceptably subjective" and "too subjective"? And are you sure it's not just a subjective code name for "the thing I don't like"?
Ultimately, people practice mathematics mostly for abstract reasons. It's not a field where you routinely ship products and get rich by meeting market demand. If 99% of contemporary mathematicians don't want to become prompt engineers, there's nothing that makes the transition to AI math inevitable. If not mathematicians, the only party with vested interest in that would be the PR departments of frontier labs.
Agreed, mathematics is ugly without ai. I feel beauty is in massive complexity and intricacy. Every time I see a small proof it feels too easy and trivial. Triviality and simplicity is ugly to me.
> One could argue for pure mathematics that is of no practical utility
wait what is the math with no utility
the analogy with experimental physics is a good one - being sure something is true is a good first step to developing an elegant proof of its truth.
I think what people find beautiful in math is largely something that enables the mathematics (or physics) to be translated to something that they can think about intuitively, and what people can handle in an intuitive way is largely an artifact of what the brain evolved to be able to think about "naturally". But it's quite possible that most things that are true about the universe or math are just ugly and unintuitive, and the pursuit of truth shouldn't necessarily be limited by what people can easily reason about and hold in their heads.
Beautiful explanations are lovely when they exist, but we shouldn't wait for them if we can also find the truth through an ugly method.
More accurate title would be "Terry Tao Became an Evangelist for Lean"
Quantamagazine is essentially Renaissance Fund, which is heavily invested in AI.
This is a clever piece reminding people of Tao's pre-AI Lean efforts. Now, however, Tao and especially Gowers are receiving AI money and have AI positions so they are far from unbiased.
Or maybe they have caught Feynman's "computer disease"? Either way, this is a hype piece.
Ahem. Define "Pre-AI". Automated theorem proving has been an AI task right from the very beginning with Simon and Newell's Logic Theorist, presented at the Dartmouth workshop in 1956.
Logic Theorist soon proved 38 of the first 52 theorems in chapter 2 of the Principia Mathematica. The proof of theorem 2.85 was actually more elegant than the proof produced laboriously by hand by Russell and Whitehead (2026-03-20: What is called here Theorem 2.85 is, in fact, numbered as 2.53 in the page 107 of the 1963 Cambridge University Press edition (https://www.uhu.es/francisco.moreno/gii_mac/docs/Principia_M...) and which appears, under the same 2.53 number, on page 112 of the 1910 CUP Edition, according to the digitalization on wikibooks (https://en.wikisource.org/wiki/Russell_%26_Whitehead%27s_Pri...)). Simon was able to show the new proof to Russell himself who "responded with delight".[17] They attempted to publish the new proof in The Journal of Symbolic Logic, but it was rejected on the grounds that a new proof of an elementary mathematical theorem was not notable, apparently overlooking the fact that one of the authors was a computer program.[18][17]
https://en.wikipedia.org/wiki/Logic_Theorist#History
Maybe some people only understand "AI" to mean "LLMs" but, particularly in maths, LLMs ain't going nowhere without a symbolic solver (or a human mathematician) verifying their output.
Automath is also an early example.
> Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness.
Tao doesn’t seem to have been all that corrupted by the AI money. He’s signatory to the Leiden Declaration after all.
mathlib and lean are currently too cumbersome for many researchers to use in say algebraic geometry, but maybe more suitable for combinatorics where it has been applied recently.
the smartest people see AI as an incredible tool that enhances their productivity.
Just like me! I like AI because of how smart I am.
And I thought it was cocaine.