How Terry Tao became an evangelist for AI in math

That’s my interpretation of your comment, anyway.

lol

It won't be a programmer doing this work, because they will have gone the way of the dodo.

It'll be workers specific to a certain domain (e.g. engineer, architect, accountant) doing this on top of their usual work.

The software industry will collapse.

Of course problems remain in both approaches: a human or AI needs to make sure the lean proof is proving the correct translation from natural language spec to a formal theorem, or the PBT is testing the right properties translated from natural language.

Why do we need a human for this?

Why are you looking forward to this, though?

We mere mortals (I am a prof. of Maths at Uni) do not.

I think we can all be a bit grounded and understand reality as we see it -- one of the smartest living mathematicians is using an important invention. Not necessary to believe in any conspiracy theory.

Fundamentally, there is a one-to-one correspondence between mathematical proofs and programming. Proofs are isomorphic to type checking.

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

It perhaps isn't too different from LLMs being able to coherently output short, a few hundred words, pieces of prose, or code, but not being able to assemble them into functional output with constant "nudging".

Happy to be corrected on this!

AI not only provides potential to cause society to become overly dependent on it, but it's being developed by/pushed for by the same fucking people who caused our societies smartphone addiction.

Once you recognize what we've lost already, it's hard to turn off your brain and just compartmentalize this away as a "just a tool". Nothing that is adopted so widely is "just a tool," and thinking of it in those terms eliminates the ability to analyze the potential downstream effects it will cause.

That’s an Anti example. What’s a Pro example?

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.

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.

Instead, you proceed in layers of abstraction. For example

1. the main claim may rest on some set of sub-claims, as well as some local (to teh main claim) work to "patch things together"

2. each of those sub-claims themselves may require other sub-claims + local work, etc

These can be collected into a dependency graph. In lean, this is often called a "blueprint". Here is the blueprint for the formalization of the Polynomial Frieman-Rusza conjecture (now a theorem, by Gowers, Green, Manners, and Tao).

https://teorth.github.io/pfr/blueprint/

This layer of abstractions is (roughly) equivalent a different way to format mathematics. You could remove the Lean component (let alone any AI), and create such a dependency graph for a paper. I would argue this is a clearer way to format mathematics (again, ignoring both the formal verification applications of it, as well as AI).

Any mathematics paper intrinsically has a graph such as this underlying it, and tries to make the various linkages in the graph clear via prose. Prose is only so powerful a way to organize things. I'm sure you're familiar with the way early mathematicians would describe various formula (e.g. the quadratic formula) via prose. It is very hard to understand.

Separately from this dependency-graph perspective, you can do things like

1. add formal verification. Now, each component in the dependency graph is verifiable with high confidence (though harder to write and read). This has some benefits and downsides. Harder to write and read is bad. Being able to have high confidence in the veracity of the result is *very* good. It allows larger collaborations in mathematics. Previously, a large collaboration would require all mathematicians to trust eachother to a large extent. This is (practically) difficult.

2. when each component can now be verified to high accuracy, you can now throw AI at it. I won't extoll the virtue of this. There are parts of it that seem interesting, but many "AI for Math" things currently are stil producing unformalized papers (in prose).

Maybe the main thing I'd say is that this type of "graph structure, with each component trusted" is already implicitly what mathematicians do. You write papers that cite other papers etc. Except now, instead of needing to look for status signals to trust papers (or invest personal effort), you can look for another (honestly fairer) signal to trust papers. So there's a sense in which formalization allows for the democratization of mathematics. I do think there's something beautiful about that.

wait what is the math with no utility

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.

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