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.

Do you mean RenTech? Not sure how you'd know they're heavily invested in anything given the notorious secrecy of the firm. Maybe their public funds have invested in AI, but their most recent 13F shows a 23% tech sector allocation, and their public funds are maybe only half of their total AUM.

Regardless, doubting the legitimacy of Quanta bc it's a Simons Foundation initiative is foolish.

Tao doesn’t seem to have been all that corrupted by the AI money. He’s signatory to the Leiden Declaration after all.