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.
Regardless, doubting the legitimacy of Quanta bc it's a Simons Foundation initiative is foolish.