6 ms·

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, how

by klmarks 3mo ago

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.

TimorousBestie 3mo ago
Tao doesn’t seem to have been all that corrupted by the AI money. He’s signatory to the Leiden Declaration after all.
- bmitc 3mo ago
  Doesn't that require you to just click a few buttons? It's not like it's a binding pledge.
YeGoblynQueenne 3mo ago
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_Mathematica_vol1.pdf 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_Principia_Mathematica/Part_1/Section_A#Discussion_2 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 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.
- lioeters 3mo ago
  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.
dogmayor 3mo ago
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.

by klmarks 3mo ago

TimorousBestie 3mo ago

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

bmitc 3mo ago
Doesn't that require you to just click a few buttons? It's not like it's a binding pledge.

YeGoblynQueenne 3mo ago

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_Mathematica_vol1.pdf 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_Principia_Mathematica/Part_1/Section_A#Discussion_2 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 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.

lioeters 3mo ago
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.

dogmayor 3mo ago

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.