AI-Generated Mathematical Results and the New Verification Crisis

On 6 October 2026, OpenAI released 722 mathematical manuscripts, organised into 372 families of related results. Those figures count manuscripts and result families, not 722 new theorems already accepted by the mathematical community. OpenAI says the material is at different stages of verification and that not every manuscript has an accompanying Lean formalisation. On 7 October, the Association for Human Mathematics published a statement on Terence Tao’s blog criticising the mass release and arguing that mathematical research should remain centred on human understanding. It was a guest statement signed by the association, not Tao’s personal verdict on every manuscript. [1, 2, 3]

The release raises a specific question. AI can produce mathematical claims and proof texts rapidly. Can people establish their correctness at the same pace, and understand what they mean for mathematics? I think this could become a new crisis in the development of the field. To see where the difficulty lies, we need to distinguish generating a result, verifying a proof and understanding a method.

AI outputs in different fields meet different standards. We can judge an image, a piece of music or a literary work by its effect without reconstructing how it was made. A program can be run and tested against some inputs, although passing those tests does not guarantee correctness for every input. Engineering and experimental science must also ask whether a result holds under real conditions and whether independent experiments or observations support it. Verification matters in these fields too. A useful output does not, by itself, make its factual claims or reasoning reliable.

A mathematical theorem makes a stronger claim. Under stated definitions and assumptions, it says that a conclusion holds for every object within a specified domain. Many computed examples can support a conjecture, but they generally cannot replace a proof. Even a million confirming cases leave open the possibility of a later counterexample. Observations can lead an empirical science to revise a theory; a general mathematical claim calls for a valid deduction from its premises.

There is also an asymmetry between a counterexample and a general proof. For a conjecture saying that every qualifying object has a certain property, one rigorously checked counterexample is enough to refute it. Finding such an example may be hard, however, and one must still establish that it meets every condition. An AI-discovered counterexample can therefore be a genuine mathematical contribution. It does not follow that most AI-generated mathematical results are counterexamples, or that negative results are always easy to verify.

Mathematics has another distinctive feature: theorems have explicit dependencies. One result may become a premise in the proof of another. If an insufficiently checked claim is treated as an established theorem, an error can spread through those dependencies. This release provides a concrete example. OpenAI’s revision history records that, on 7 October, a sign error invalidated a crucial argument in one algebraic geometry manuscript. Two manuscripts dependent on that construction were withdrawn with it. This does not show that the remaining manuscripts are faulty. It does show why a count of released documents is not a count of confirmed mathematical advances. [4]

I initially described AI as a black box, but that description needs a clear boundary. How a model internally searches for and arrives at a result is one question; what proof it submits is another. We generally cannot reconstruct its entire internal path of discovery from an output. That does not mean it cannot provide a proof we can check. OpenAI has released abridged reasoning summaries for some results and formal proof material for many of them, while acknowledging that verification does not cover the whole collection. [2]

Human mathematicians may also reach a conclusion through intuition, analogy or chance before writing a proof. We do not need to reconstruct the discovery process inside the mathematician’s mind to accept the theorem. We do need to examine the public argument. The strongest reason to question an AI-generated claim is therefore a lack of adequate grounds for accepting it. An opaque discovery process makes research and explanation harder, but does not by itself refute the conclusion.

Formal proofs can address part of the problem. Tools such as Lean check a formalised proof against explicit rules. Here AI can generate a candidate proof while a dedicated proof checker tests whether it passes. That is fundamentally different from asking another chatbot whether the argument looks right. Checking a mathematical proof need not mean asking people to retrace every formal step by hand. Restricting all verification to manual work would overlook what formalisation can do.

Formal checking also has a definite limit. It verifies the statement entered into the system and a proof of that statement. Someone still has to check whether the definitions are accurate, the assumptions are complete and the formal statement matches the problem the paper claims to solve. If the original problem concerns every object but the formal theorem adds a restriction, a successful check does not settle the original problem. In an essay published on Tao’s blog, mathematician Thomas Hales stresses that the formal statement must be audited against its intended meaning. He also notes that this task is generally far easier than checking the entire proof by hand. [5]

Correctness and understanding need to be distinguished as well. A complete and reliable formal proof does not cease to be valid because it is long or lacks a simple explanation. But people may still struggle to see why it works, which structure matters, whether its assumptions can be weakened and whether its method applies elsewhere. Establishing a theorem and turning its proof into a method that can be taught, changed and extended are different achievements.

Traditional mathematical research has tended to connect these activities. As mathematicians search for proofs, they often develop an understanding of the methods, then bring that understanding into shared knowledge through writing, discussion and review. The process is imperfect; no one needs to understand every proof. Yet for a significant result to become useful, someone needs to explain its main steps, assumptions and applications. Mass AI generation can separate these tasks. Claims and proof texts may appear first in large numbers, leaving others to verify them, explain them and work out their place in the field.

That is the practical problem when generation outpaces manual verification. Expert reading may remain a bottleneck for manuscripts without formal proofs. For reliably formalised results, the step-by-step check can be faster, but checking the intended statement and understanding the method still take time. Tao’s public writing on AI likewise distinguishes generation, verification and the subsequent digestion of a result. Faster generation and verification do not necessarily make understanding faster. [6]

A persistent gap in speed would have consequences. Unconfirmed claims would accumulate, making it harder to know which results can safely be cited. Specialists might spend so much time checking large volumes of claims that their own research suffers. Even formally checked proofs could remain unexplained, allowing the number of theorems to grow without a comparable accumulation of methods people can use. If those generating results announce how many problems they have “solved” without taking responsibility for revision and explanation, they shift a substantial share of the research work onto the wider community.

Those consequences could amount to a crisis in mathematical practice. They do not show that the logical foundations of mathematics have failed. Rapid generation does not invalidate a valid proof, and an unverified claim is not automatically false. A release of hundreds of manuscripts raises a serious question about verification capacity; its size alone cannot establish that verification across the whole field has already fallen behind. What matters is whether unverified results keep accumulating, whether errors propagate through citations, and whether reliable proofs become understood and useful in further research.

Publishing an AI-generated mathematical result should therefore involve a clear statement of the claim, its assumptions, its proof dependencies and the scope of verification. A claim of formal checking should come with the precise formal statement and materials others can check. Those releasing the work should also explain the key method, respond to criticism and maintain a record of corrections. Mathematics can use machines for extensive rule-based checking while people focus on whether the right question was proved, what the method tells us and what further work it enables.

My judgement is that we should neither accept AI-generated mathematical claims blindly nor reject them solely because AI produced them. The new risk for mathematics is that mass generation breaks the connection among claims, proofs, verification and understanding. If generation remains faster than the capacity to verify and understand what it produces, the immediate result may be a large backlog of claims rather than a comparable body of reliable knowledge. Any account of mathematical progress must include the work that follows the initial result.

Sources

[1] https://community.openai.com/t/first-look-at-mathematics-manuscripts-from-an-internal-frontier-model-at-openai/1403886
[2] https://openai.com/index/sharing-ai-progress-in-mathematics/
[3] https://terrytao.wordpress.com/2026/10/07/ahm-statement-on-openais-october-6-release-of-mathematical-documents/
[4] https://github.com/openai/math/blob/main/history.md
[5] https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/
[6] https://teorth.github.io/tao-web/ai-views.html