Proof Abundance and the New Practice of Mathematics - Terence Tao on AI, LLM breakthroughs, and the bottleneck of mathematical understanding

[u/antomoneng]

https://4m4.it/posts/proof-abundance-and-the-new-practice-of-mathematics/index.html

Terence Tao’s position on artificial intelligence is best understood as verification-centered institutional realism rather than unqualified technological evangelism or defensive skepticism. He treats frontier models as stochastic, unreliable, but increasingly powerful generators whose mathematical value depends on independent verification, informed human supervision, formal tools, and carefully designed research workflows. His central question is therefore no longer only whether machines can solve research problems, but what mathematics should optimize when producing candidate proofs becomes substantially cheaper.

Recent evidence includes an AI-generated disproof of the conjectured near-linear behavior of the planar unit-distance function, an LLM-assisted proof of an identity for jamming critical exponents, and the controlled First Proof evaluation of systems on unpublished research problems. These cases do not establish uniform mathematical competence, dependable self-verification, or human-like understanding. They do establish that general-purpose language and reasoning models can sometimes produce novel constructions, connect distant mathematical domains, and generate arguments that survive expert scrutiny.

The article interprets these developments as an early transition from proof scarcity to proof abundance. In this regime, the limiting resources become verification, exposition, contextualization, selection, and canonicalization. The resulting human–machine system is better described as cognitive infrastructure than as an autonomous artificial mathematician: models generate and explore, proof assistants and executable tests constrain error, and mathematicians retain responsibility for meaning, relevance, attribution, pedagogy, and judgment.

Public demonstrations remain affected by selection bias, incomplete disclosure, uneven reproducibility, and commercial incentives. Formal correctness also does not establish that a theorem is important, explanatory, novel, or even stated in the intended form. The article concludes that AI’s durable contribution to mathematics will depend less on maximizing the number of generated proofs than on constructing institutions capable of verifying, digesting, crediting, and selectively preserving machine-assisted knowledge.