The response of the mathematical community to artificial intelligence tools capable of performing research-level mathematical tasks. This page covers the institutional and epistemological questions raised when AI systems can generate, verify, and formalize proofs — not whether they can, but what the community should do about it.

The Working Hypothesis

Terence Tao’s 2026 ICM essay “Mathematics in the age of AI” frames the discussion by conditioning on what he calls the Working Hypothesis: AI tools will, reasonably soon, become capable of performing a reasonable fraction of research-level mathematical tasks, with reasonable levels of success, quality, supervision, and cost.¹ This is not a claim that the capability exists today — it is a conditional analysis of what happens if it arrives.

The First Proof project provides controlled evidence that this hypothesis is not science fiction: in its second batch (May 2026), seven of ten novel research-level problems were solved at publication-level quality by at least one AI system, with compute costs of tens to hundreds of dollars per problem.²

The Problem-Solving Pipeline

Tao deconstructs the goal of “problem solving” into a five-stage pipeline, each stage representing an implicit value that AI disrupts differently:

1. Generation — producing a candidate proof. AI is already strong here.
2. Verification — checking correctness. Formal proof assistants (Lean, Rocq, HOL) accelerate this.
3. Exposition — communicating the result clearly. AI output is often superficially polished but obscures the interesting parts.
4. Community acceptance — digestion by other mathematicians. Slow, human, and irreducibly social.
5. Canonicalization — absorption into definitive textbooks and reference material. The slowest and most valuable stage.

The pipeline reveals that the community’s explicit goal (“solve problems”) is a proxy for a much richer set of implicit goals. When AI optimizes for the proxy, the other goals suffer — a direct application of Goodhart’s law.³

Proof Scarcity to Proof Abundance

If the Working Hypothesis holds, mathematics transitions from an era of proof scarcity to an era of proof abundance. The institutions designed for scarcity — journals, priority conventions, hiring criteria, prizes — behave poorly under abundance:

• AI-generated proofs accumulate faster than they can be verified
• Verified proofs accumulate faster than they can be given readable write-ups
• Peer review, dependent on volunteer expert labor, is overwhelmed
• Published proofs become too numerous to work into definitive form

Tao calls this “proof indigestion” and argues that the community must shift emphasis from proof generation to proof digestion: exposition, refereeing, publication, and canonicalization.⁴

The Leiden Declaration

Published June 2, 2026, and endorsed by the International Mathematical Union, the Leiden Declaration on Artificial Intelligence and Mathematics is the community’s first systematic response.⁵ It arose from a September 2025 workshop at the Lorentz Center in Leiden and consists of 23 recommendations across four constituencies.

Core values identified

• Proof confers the highest degree of certainty and understanding
• Results are attributable to specific authors who take credit and responsibility
• Arguments are transparent and independently verifiable
• Shared standards of depth, difficulty, and significance
• Mathematics produces understanding, clarity, and judgment in human communities

Key recommendations for individuals

• Disclose tool use — include a “Tool and computational resource disclosure” section in papers
• Support reviewing — make it easier for peers to review AI-assisted work
• Retain responsibility — correctness remains exclusively with human authors
• Affirm humanity of authorship — credit belongs to humans, not automated systems
• Proper attribution — proactively find and credit sources, even when AI obscures them
• Consider carefully which tools to use — some tools align with the Declaration’s values, others do not

Recommendations for organizations and policymakers

• Maintain standards of rigor for automated techniques
• Protect authors’ rights (training-data consent, opt-out clauses)
• Insist on peer-reviewed publication venues
• Support public research laboratories independent from industry
• Regulate the AI industry and invest in public computational infrastructure

Threats identified

1. Unreliable results — plausible but incorrect arguments difficult to distinguish from correct proofs
2. Attribution breakdown — models trained on published works without proper citation
3. Incentive disruption — hiring, funding, and recognition distorted by AI access
4. Informal communication — press releases and blog posts replacing peer review
5. Loss of autonomy — research directions shaped by commercial feasibility rather than mathematical significance

The Cowen Counterpoint

Tyler Cowen’s response to the Declaration and Tao’s essay argues that the main “action variable” is not the decisions of AI companies but how well mathematicians adapt to the new reality.⁶ He expects funding and interest in mathematics to rise, and criticizes the complaint as premature: “I didn’t like the first week or two of your intellectual revolution” is not a sufficient basis for policy. Cowen draws an analogy to his own position as an economist facing AI: the correct response is to adapt one’s intellectual portfolio, not to demand that companies manage the disruption.

This counterpoint highlights a genuine tension in the Declaration: it assigns significant responsibility to AI companies and policymakers, but the most immediate agency lies with the mathematical community itself — in what it rewards, how it trains students, and what it counts as a contribution.

Open Questions

• How should the community handle AI-generated proofs that are verified but not understood by any human? Tao’s rule of thumb: if the authors cannot give a clear, expert-level talk on their results, the result should not be published — a proof no human can explain is incomplete, even if formally verified.⁷
• Can new institutions (collaborative formalization projects, structured problem databases, venues for negative results) absorb proof abundance without collapsing under it?
• Will the Leiden Declaration’s recommendations be adopted by journals, funders, and universities, or remain aspirational?
• What happens to mathematical training when AI can produce correct homework? Tao argues education must emphasize the irreducibly human aspect of the work.

Connections

• satisfiability-modulo-theories — formal verification tools (Z3, Lean) are the technical substrate of AI-assisted proof
• eval-awareness-and-grader-orientation — Goodhart’s law operating inside AI systems and in the metrics used to evaluate them
• ai-agent-capitalization-and-institutions — how institutions shape and are shaped by AI capabilities
• technological-unemployment-history — historical parallels: when machines displaced artisanal labor, the adjustment fell on new entrants, not incumbents
• ai-economic-growth-complementarity — Cowen’s centaur-transition prediction for the intelligence sector, with mathematicians as the live case

Sources

• Terence Tao 2026 — Mathematics in the age of AI
• Alper, Barany, Chavarri Villarello, Dahmen, Dean, Ganapathy, Harris, Holmes, Jamnik, Kelk, Kra, Martin, Naskręcki, Ochigame, Portegies, & Schmitt 2026 — Leiden Declaration on Artificial Intelligence and Mathematics
• Tyler Cowen 2026 — The mathematicians rebel against AI
• Nature editorial 2026 — Mathematicians are developing rules for AI use — other fields should follow

Footnotes

1. raw/papers/tao-mathematics-age-ai-2026.md ↩

2. raw/papers/tao-mathematics-age-ai-2026.md ↩

3. raw/papers/tao-mathematics-age-ai-2026.md ↩

4. raw/papers/tao-mathematics-age-ai-2026.md ↩

5. raw/articles/leiden-declaration-ai-mathematics-2026.md ↩

6. raw/articles/cowen-mathematicians-rebel-ai-2026.md ↩

7. raw/papers/tao-mathematics-age-ai-2026.md ↩