News · 2026-10-12

Terence Tao proposes Math 2.0 for an age of abundant proofs

Terence Tao has proposed a “Math 2.0” agenda that uses AI to build mathematical understanding and shared research infrastructure alongside producing proofs. Presented at Caltech on October 9 and posted October 10, the proposal asks how mathematics should organize itself if proofs become much easier to generate. It treats explanation, judgment and transparent evaluation as essential research work.

Key facts

• Tao’s 29-page deck lays out a program for mathematical work under growing proof abundance.
• The Caltech lecture occurred October 9, followed by Tao’s October 10 public post.
• One cited project established 22,028,942 implication edges, not that many independent open-problem solutions.
• The primary sources are Tao’s dated post and his lecture slides.

A theorem can be correct without making its importance or useful mechanism clear to the next person. That distinction becomes harder to ignore when a system can produce results faster than a community can read them. Tao’s lecture makes this a question about the goals of mathematics, rather than a contest over whether any particular model deserves a high score.

The Caltech event listing retained the earlier title, Machine Assisted Proof. Tao explains that the talk had been planned well in advance and its framing changed with recent developments. The public deck’s title, “Math 2.0,” captures the expanded agenda: what institutions reward, what infrastructure researchers share, and how understanding moves between people.

His starting point is that solving difficult problems has often served as a useful signal of deep mathematical understanding. When solutions are scarce, the search creates knowledge about methods, examples and failed approaches. Tao argues that abundant machine-produced proofs could weaken the connection between solving a problem and obtaining the human understanding the discipline values.

Think of a solved problem as a destination on a map. Reaching it is valuable, but so are learning the terrain, discovering connecting roads and making a route other travelers can follow. An automatically delivered destination does not necessarily supply that reusable map. This is an analogy for Tao’s institutional argument, not evidence that machine-produced proofs are inherently uninformative.

The proposals are concrete. AI could help build large, machine-checkable surveys of mathematical structures, create clearer expositions of already-proved results, connect papers in living research networks and expand formal libraries. It could investigate nearby theorems by changing assumptions, test which inputs a result actually needs, and help researchers identify methods that travel between problems. The established lesson on proof assistants explains the checking machinery behind part of that program.

A numerical example illustrates the difference between scale and headline inflation. The Equational Theories Project paper reports 22,028,942 implication edges among 4,694 simple algebraic laws. Human-generated and automated proofs were validated in Lean. These are relationships in a mathematical graph, not 22 million famous open problems independently solved by AI. Tao uses the project to illustrate a different shape of collective mathematical work.

The deck also discusses a crowdsourced challenge covering 25,000 possible transitive Galois groups at degree 24. That slide does not attribute the completed stage to AI. Its relevance is organizational: large coordinated projects can create shared maps and datasets that isolated theorem production does not. Readers should resist converting every impressive number in an AI-era lecture into a model performance claim.

The institutional implications extend to the next generation of researchers. If prestige follows only completed problems, work that helps others understand a result can be undervalued. Tao’s proposed exposition and infrastructure projects supply alternative research objectives, though the deck does not establish how institutions would fund or reward them.

Tao asks capability assessments to include resource use and negative results. That would make it easier to distinguish broad performance from carefully selected successes. Ground Truth’s earlier reporting on OpenAI’s mathematical release and withdrawals supplies related context for why review histories and explicit correction records matter.

The strongest counterargument appears in the Hacker News discussion. Commenters challenge Tao’s hypothetical cancer example: effective treatments often reach practice before their mechanisms are fully understood, and robust trials can justify use. That objection identifies the potential cost of demanding complete understanding before accepting benefits. It does not settle the separate mathematical question of what knowledge a field wants to preserve.

The proposal’s limit is that it is an agenda, not a demonstrated solution to the institutional problem. It does not measure how much AI-generated work is understandable, how quickly people can absorb it, or which incentives would work best. Its significance is to make those questions explicit. If proof production accelerates, funding and prestige attached to explanation, shared tools and careful evaluation may become more consequential than another count of completed manuscripts.

Primary source, verified: read the paper →

Ground Truth. (2026, October 12). Terence Tao proposes Math 2.0 for an age of abundant proofs. Ground Truth. https://groundtruth.day/news/terence-tao-math-2-0-understanding-agenda.html

@misc{groundtruth:terence-tao-math-2-0-understanding-agenda,
  title  = {Terence Tao proposes Math 2.0 for an age of abundant proofs},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {oct},
  url    = {https://groundtruth.day/news/terence-tao-math-2-0-understanding-agenda.html}
}

Topics: mathematics · ai-science · verification · research-culture