Should AI Labs Release Proofs Before Humans Check Them?

1 November 2026 · 6 min

A pile of preprints, a proof assistant, and the referees left to sort them out.

On the evening of 6 October, while mathematicians were gathered at the Institute for Advanced Study to open the academic year, OpenAI put 722 preprints covering 372 distinct results on a website. They came from an unreleased internal model that, according to the company, was given about 4,000 problems and spent an average of roughly three hours of ChatGPT Pro "thinking" on each result. Within a day, OpenAI withdrew three of them because of a sign error.

I referee papers, and I write papers that other people referee. My first reaction wasn't awe or outrage. It was a tired question: who is going to read all of this?

What was actually released

The catalogue, hosted on GitHub, groups manuscripts into "families": a main result plus companion arguments, consequences, or alternative proofs. As of 7 October, 300 of the 719 remaining top-line results had Lean formalizations, about 42%. Implicator also reports that OpenAI itself says some of the unformalized results could have issues, and that an OpenAI spokesperson said many of the new results are not yet understood by the company's own mathematicians.

The reactions were mixed. Scientific American quotes NYU's Roland Bauerschmidt describing some of the papers as "sort of this AI slop" and saying, "If I had received these by e-mail from a nobody, I probably would have deleted it, it's so badly written." MIT's Andrew Sutherland was more measured: "While I expect most of these will ultimately be found to be correct, or at least correctable, we should expect some of the proofs to contain mistakes, possibly serious ones." A month before the release, Thomas Kahle had observed on Mastodon that "There is an anti-AI group among mathematicians who want nothing to do with it." Others are already formalizing, checking, and rewriting the results.

Why "42% Lean-checked" means less than it sounds

Lean is a proof assistant. If a proof compiles, every logical step from the hypotheses to the stated conclusion has been checked by a small, trusted kernel. That is a much stronger guarantee than any referee report I have written. Human refereeing is sampling. We check the steps that look dangerous and trust the ones that look routine.

But Lean checks the statement as formalised. It doesn't check that the formal statement is the theorem the English paper claims, or the open problem the paper says it solves. A definition with an off-by-one, a missing hypothesis, or a quietly weaker conclusion can give you a perfectly verified proof of the wrong thing. Science quotes Steven Sivek, a member of the Association for Human Mathematics, saying that in some cases what was formalized is "something weaker" than the main theorem, and reports that a recent preprint found the Lean formalization of OpenAI's earlier Navier–Stokes result doesn't match the proof described in the accompanying paper.

So the real picture is this: for 42% of the results, a machine has checked something. Whether that something is the advertised theorem is still a human question. For the other 58%, we have informal proofs from a model that even its owners say may contain problems.

The sign error

The withdrawal notice is worth reading in full, because it is a good example of how mathematics fails. In "Algebraicity of Weil classes on split abelian eightfolds", the proof gave each reverse stabilization trace the sign +1. Once you account for the orientations of the cusp's two branches, it should be −1. The signed double-point count comes out as −2m instead of zero, so the hypothesis of the Eliashberg–Murphy cancellation theorem fails, and everything built on it collapses. Two dependent papers on Kuga–Satake correspondences and the rational Hodge conjecture for products of K3 surfaces went down with it. OpenAI also revised 14 other manuscripts.

Credit where it's due: the notice is precise and honest. It says the withdrawal "concerns the proof; it does not assert that the mathematical statement is false." Many human authors handle their errors worse. But note what happened. Humans found the error, quickly and for free, in a field where checking a single paper can take a specialist weeks.

The case for releasing anyway

There are real arguments for putting everything out at once, and I take them seriously.

Speed. If even a fraction of these results are right, sitting on them for a year of private checking delays the field.
Transparency. A public dump with a public revision history is better than a lab quietly keeping its best results, or announcing only the wins.
Community checking works. The sign error turned up within a day. That is the open-review argument proving itself.
arXiv norms. Mathematicians post unrefereed preprints all the time. Preprints are claims, not certified truths, and everybody knows it.

The case against

The arXiv argument breaks down on scale and accountability. When I post a preprint, my name is on it. I understand it and can defend it at a seminar, and I have every reason not to embarrass myself. A human writes a handful of papers a year. A lab can now produce hundreds in a day. By the company's own account, its own mathematicians don't yet understand many of them, and outsiders can't rerun the model.

Checking costs money even when no one is paying for it. Every hour a specialist spends on a badly written AI manuscript is an hour taken from their students, their own research, or the human-written paper sitting in their referee queue. Flooding a commons with claims and letting volunteers sort them is a choice about who carries the cost. Then there is credit. If an expert repairs a gap or untangles an unreadable proof, does anyone count that work? Right now the headline says "372 open problems" and the checking happens in the footnotes.

What I'd propose

I don't think "never release before humans check" is the right rule. It is unenforceable and would give up real benefits. What I'd ask for is this:

Verification status on every result, not the catalogue as a whole. Each theorem should be tagged as one of: Lean-checked with the formal statement reviewed by a human against the English one; Lean-checked with the statement not yet reviewed; informal only; or under revision. "42%" should never stand in for "verified."
Release in stages. Put out the Lean-checked, statement-reviewed results first. Hold the informal ones until at least one named expert has read each, or label them clearly as unchecked conjectural proofs.
Pay and credit the checkers. If a lab gets the headline, it should fund the referees: paid review, public acknowledgment, citable checking reports.
Make it reproducible. Publish prompts and compute per result, as the advisory group hosted at the Institute for Advanced Study asked, so OpenAI's claim that nearly every result came from a single prompt to a single agent is something people can test and not just take on trust.

My answer

Should AI labs release proofs before humans have checked them? They can release claims before humans check them, the same way any of us posts a preprint. But they shouldn't present those claims as results, put an unverified count in the headline, or leave the checking to unpaid strangers. Release what is machine-checked and human-read first. Clearly label everything else as unverified. Pay the people who do the checking. Proofs don't become valuable when they are written, whether by a person or a model. They become valuable when someone understands them, and the labs should take responsibility for that step too.