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.

The October 2026 OpenAI Bulk Release

The Working Hypothesis stopped being hypothetical in the fall of 2026. After a September controversy over a claimed Navier–Stokes solution — disputed on priority grounds by Tristan Buckmaster, whose recent Euler-equations results may have leaked into OpenAI’s prompts — twenty-eight Fields medalists signed “A Severe Misalignment of AI in Mathematics” (September 11), warning against AI companies treating unsolved problems as benchmarks without enhancing human understanding. On October 7, OpenAI released 722 manuscripts covering 372 open problems across algebra, number theory, theoretical computer science, logic, and topology, produced by an internal unreleased model and posted to GitHub without prompts or runtime details. Three papers were retracted within a day; verifying the corpus is expected to take months.⁷

The release fell short of the norms the field had just finished writing down. The Advisory Group on Mathematics and Artificial Intelligence (AGMAI) — nine researchers hosted by Princeton’s Institute for Advanced Study, whose first request was to stop evaluating proprietary models on open problems — had issued guidelines in late September. By TechCrunch’s accounting, only ten of the manuscripts included the model’s chain of thought and 42% of the proofs had not been formalized in Lean; the group had also asked for machine-readable metadata correlating natural-language proofs with their formal artifacts, which the release lacked. A Cambridge–King’s College paper the same week documented “lost in translation” discrepancies between OpenAI’s natural-language Navier–Stokes proof and its Lean formalization, concluding that autoformalized proofs should not be trusted without ordinary peer review.⁸

Reactions split along the now-familiar line. Martin Bridson, president of the Clay Mathematics Institute, called the release “breathtaking”; Scott Aaronson compared the mathematician’s position to a hunter-gatherer watching a resort hotel with a helipad rise next door. Andrew Sutherland set the replication bar: “Until and unless they release the model and people can replicate their results, I think you should treat any claims about one-shotting problems with a single agent as unverified.” Melanie Wood, an AGMAI member, called the release “the beginning, not the completion, of the process of human understanding and the incorporation of the work into mathematical knowledge”; Terence Tao crystallized the digestion problem — problems “are being solved autonomously by AI prompters who have no interest in the broader field itself once their initial target is ‘solved’.”⁹¹⁰

The event sharpens this page’s questions rather than answering them. The Leiden Declaration’s “informal communication” threat is now concrete; so is Tao’s “proof indigestion,” and with it a new funding question — AGMAI’s suggestion that labs bankroll the human assimilation of their models’ output is the first proposal for an assimilation line item. The hermeneutic reading of the moment — mathematics as a discipline of reading and understanding machine-generated texts — is developed under fusion-of-horizons; the institutional-struggle reading under habitus.

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.
• After the October 2026 release: who pays for assimilation? AGMAI proposed that labs fund the human mathematicians needed to make machine output meaningful; no lab has committed.¹²

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
• fusion-of-horizons — the hermeneutic frame for the post-release work: reading machine proofs as a fusion of horizons
• habitus — the Bourdieusian frame: the field’s response as an orthodoxy fight

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
• 2026 — OpenAI bulk release of mathematical papers (Wikipedia)
• Tim Fernholz 2026 — OpenAI’s math solutions aren’t meeting the field’s standards yet

Footnotes

1. Terence Tao 2026 — Mathematics in the age of AI ↩

2. Terence Tao 2026 — Mathematics in the age of AI ↩

3. Terence Tao 2026 — Mathematics in the age of AI ↩

4. Terence Tao 2026 — Mathematics in the age of AI ↩

5. 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 ↩

6. Tyler Cowen 2026 — The mathematicians rebel against AI ↩

7. 2026 — OpenAI bulk release of mathematical papers (Wikipedia) ↩

8. Tim Fernholz 2026 — OpenAI’s math solutions aren’t meeting the field’s standards yet ↩

9. 2026 — OpenAI bulk release of mathematical papers (Wikipedia) ↩

10. Tim Fernholz 2026 — OpenAI’s math solutions aren’t meeting the field’s standards yet ↩

11. Terence Tao 2026 — Mathematics in the age of AI ↩

12. Tim Fernholz 2026 — OpenAI’s math solutions aren’t meeting the field’s standards yet ↩