Why Mathematicians Are Pushing Back on AI-Generated Proofs

A proof used to arrive as a stack of pages, a chalkboard covered in arrows, and a colleague willing to spend a month looking for one missing step. In September 2026, a new kind of proof arrived with a very different origin: thousands of software agents exploring a problem in parallel.

On September 8, OpenAI said an internal system had produced a proposed solution to the Navier–Stokes existence and smoothness problem, one of seven famous problems selected by the Clay Mathematics Institute, with a $1 million prize attached to each accepted solution. The announcement followed claims in May about the unit-distance problem, a long-running geometry conjecture, and in August about ten other advances in mathematics and theoretical computer science. Three days later, a public declaration signed by leading mathematicians warned that the race to use open problems as artificial intelligence benchmarks could damage the discipline itself.

Why are mathematicians upset with AI in mathematics? The short answer is not that they reject computers. Mathematicians have used computer programs that manipulate formulas, numerical experiments, and proof assistants for years. The argument is about what a mathematical result should provide: not only a true conclusion, but understanding, credit, and a trail other people can inspect.

The technical method is more than a chatbot

The Navier–Stokes claim did not come from asking a chatbot to solve a famous equation once. OpenAI describes a multi-agent system. A software agent is a model assigned a goal and given tools, memory, or the ability to run code. A multi-agent system lets many such workers explore different strategies, exchange promising ideas, and have a coordinator assemble the strongest pieces.

OpenAI says roughly 10,000 agents worked concurrently on the problem. The agents reached their proposed resolution after about 88 hours, followed by 17 hours of formalization, meaning the argument was translated into a machine-readable language and checked. This is an example of test-time compute: the amount of computation spent on a particular problem after a model has already been trained.

The basic pattern looks like this:

for strategy in many_strategies:
 draft = agent.explore(problem, strategy)
 if lean_checker.accepts(draft):
 candidates.append(draft)

This is a conceptual sketch, not a working program. Its important idea is the separation between discovery and verification. The model generates possible arguments; a stricter system rejects steps that do not follow from the rules.

Lean is a proof assistant, meaning software that checks a mathematical argument written in a precise formal language. A formal proof is not a paragraph that sounds convincing. It is a machine-readable sequence of definitions, assumptions, and deductions that a checking program can inspect. That makes Lean valuable, especially for long arguments where a human reader could overlook a sign error or an unstated condition.

But a green check mark does not answer every question. The checker verifies the statement that someone encoded. It does not decide whether that statement captures the mathematical idea people intended, whether the result connects to the rest of the field, or whether the proof has been explained in a form a student can learn from.

Correct is not the same as understood

This distinction is the center of the current dispute. Mathematics prizes proof because proof gives certainty and, ideally, explains why a result is true. A machine may find a valid chain of deductions without revealing a useful concept in a human-sized form.

Imagine receiving a 40,000-line formal proof that establishes a remarkable theorem. It may be completely correct. Yet the next mathematician still needs to know which lemma matters, why the construction was chosen, and where the same trick might work again. Those are not cosmetic questions. They determine whether a result becomes a tool or remains a sealed box.

The timing matters too. The Clay Mathematics Institute’s rules for a Millennium Prize solution require publication in a qualifying outlet, at least two years of waiting, and general acceptance by the mathematical community. OpenAI says it is not claiming the prize for its Navier–Stokes result. That restraint is significant: a company announcement, a paper, a formal certificate, and a settled theorem are four different stages.

The uncomfortable problem of credit

The declaration’s sharpest concern is attribution. Large language models, systems trained on enormous collections of text, draw on mathematical papers and formal libraries as part of the wider human record. When a model produces an idea that resembles earlier work, tracing the path back to the people who developed the underlying techniques can be difficult.

The Navier–Stokes episode made that problem visible. OpenAI says it began its effort after hearing a rumor connected to work by NYU mathematician Tristan Buckmaster and Anthropic researcher Levent Alpöge. OpenAI later said its system had not seen their work and that the proofs were substantially different. That addresses one narrow question: possible data contamination, meaning the unintended use of another researcher’s private or unpublished material. It does not settle the larger question of how companies should behave when they learn that other researchers are close to a breakthrough.

Academic mathematics has its own version of source control. Ideas are discussed in seminars, refined in private notes, and connected to earlier papers. A rushed announcement can flatten that history into a product story: the model solved the problem, while the human network that made the problem solvable disappears from view.

The benchmark is not the whole discipline

A benchmark is a standardized test used to compare systems. Open problems look attractive as benchmarks because the outcome seems clean: a conjecture is proved or disproved, a formal checker accepts the result, and a company can point to a dramatic headline.

Yet the easiest thing to count is not always the thing worth protecting. If research rewards a flood of machine-generated true-or-false results, mathematicians may spend more time auditing output and less time developing ideas. Students may also lose part of the apprenticeship that comes from struggling with a problem, making a bad conjecture, and learning to recognize a promising dead end.

That does not make AI useless. It suggests that the best uses may be more selective: searching a huge family of cases, finding counterexamples—examples that disprove a claim—testing an argument, translating a proof into Lean, or suggesting connections between distant areas. The declaration leaves room for that kind of collaboration. Its objection is aimed at a system that treats mathematical understanding as a side effect of a score.

What responsible AI mathematics could look like

A healthier workflow would make the machinery visible. Papers should disclose which models and tools were used, how much computation was involved, and which parts were guided or rewritten by humans. A claimed breakthrough should include both a readable explanation and a formal artifact where appropriate. Prior work should be identified aggressively, even when the model cannot do that reliably on its own.

Most importantly, the community needs time. Independent mathematicians should be able to reproduce the argument, simplify it, challenge its assumptions, and decide whether it opens a new line of research. That process may feel slow beside a company’s product calendar, but slow review is not a failure of mathematics. It is part of how mathematics remembers what it has learned.

AI-generated proofs can be real proofs. The harder question is whether the surrounding process produces real mathematical progress. A result earns that description when people can verify it, understand its ideas, credit its sources, and use it to ask better questions. The machines may change how far we can search. They should not decide what counts as understanding.