_____________________
We mere mortals (I am a prof. of Maths at Uni) do not.
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.
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...
Of course, that is my view of it.
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.
*Completely made up statistic.
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?
For any practical application, you are only interested in finite set of concrete identities, so anything beyond that is surplus to requirements, surely?
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.
“Beauty will save the world”
Supposedly even drowned their member that divulged their existence.
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.
wait what is the math with no utility
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.
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.
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 ("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.