GetPack

Posted on Oct 14 Originally published at getpack.fr

Maths: OpenAI posted 722 AI proofs, 42% machine-checked

#ai #openai #math #students

First published in GetPack Magazine, sourced guides to use AI well as a student.

On October 6, 2026, OpenAI posted 722 mathematics manuscripts on GitHub, written by an internal model nobody can use. The next day, three were withdrawn: a sign error. Behind the row sits a question you meet in every problem set: at what point is a proof actually verified?

In short: the public repository openai/math holds 722 manuscripts grouped into 372 result families, using on average three hours of ChatGPT Pro thinking compute per result. On October 7, three were withdrawn after a sign error invalidated one and, by dependency, two others; 719 remain. The repository claims 42% of top-line results are formalized in Lean, but the term is defined nowhere and independent recounts land closer to 24% or 36%. For you, the interesting part is not the fight: it is learning to separate « this looks right » from « this has been checked ».

What OpenAI put online on October 6, 2026

The openai/math repository holds PDF manuscripts, Lean formalizations and abridged summaries of the model's reasoning. The README is blunt about the cost: « On average, each result used three hours of ChatGPT Pro thinking compute with that model. »

The model itself is not available. No public name, no way to test it, so no way to reproduce anything: you can read the proofs, you cannot replay the experiment.

The most discussed result concerns the quasi-Riemann hypothesis, a zero-free half-plane for every Dirichlet L-function. Nature notes, on the other hand, that the batch contains no solution to any of the five remaining Millennium Prize Problems.

Three manuscripts withdrawn the next day: one sign error

The repository changelog dates the operation to October 7, 2026. A sign error invalidates a stabilization-trace cancellation argument in « Algebraicity of Weil classes on split abelian eightfolds », posted on September 18. Two other manuscripts relied on that construction: they fall with it.

Retraction Watch laid out the details on October 8: three manuscripts withdrawn, fourteen revised, thirteen updated to cite the corrected versions. An OpenAI spokesperson says there that the company welcomes scrutiny from the mathematical community and commits to correcting errors promptly. Andrew Sutherland, of MIT, answers in the same piece: the withdrawals will be viewed positively, « but it will take a lot more than that to earn back the trust they have lost ».

Remember the mechanism, because it is universal: a sign error — the most ordinary mistake there is — at the bottom of a dependency chain, and three pieces of work collapse at once.

42%, 24% or 36%: what « formalized in Lean » actually means

Lean is a proof assistant: software that checks a formal proof really does follow from a formal statement, through a small trusted kernel. On that ground it is merciless. Mathematician Kevin Buzzard, quoted by Matt Baker of Georgia Tech, puts it in one line: « You cannot fool Lean; one learns this very early on. Lean will not accept proof by authority or proof by intimidation. »

But a formalization guarantees one thing only: that the formal proof matches the formal statement. It does not guarantee that this statement says the same thing as the English sentence in the manuscript. That is the faithfulness gap: a paper posted on arXiv in June 2026 notes that a formal statement « can typecheck and be provable, yet still encode a different theorem than the source intended ». Take « every continuous function on a compact set attains its maximum »: several Lean translations compile, but the one that drops the non-emptiness hypothesis becomes false on the empty set. Matt Baker, for his part, puts that risk below 1%.

Then there is the number. The README announces « ~42% top-line results formalized », meaning 300 out of 719. An analysis published by Pebblous shows three measures in circulation: 173 manuscripts out of 719 in the formalization catalogue, or 24%; 135 result families out of 372, or 36%; and the 42%, whose numerator of 300 « matches the length of no list this file holds », the term « top-line results » being defined nowhere. That numeric sentence appeared two days after release, replacing a much vaguer « Many, but not all, of the manuscripts have been formalized. »

In other words: even the verification rate needs verifying.

The response: AHM first, then Sophie Huiberts

On October 7, the Communications Working Group of the Association for Human Mathematics published a statement, reposted the same day on Terence Tao's blog « What's new ». Its most-quoted line: « Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power. » The AHM, founded in mid-September 2026, calls on mathematicians to stop working with OpenAI.

That position is far from unanimous: the comments under the post are sharply split. Some reject the boycott, arguing that publishing full claimed proofs anyone can check is the most exposed position an author can take.

On October 12, Tao published a guest post on the same blog by mathematician Sophie Huiberts, « This is normal bad work ». Her charge sheet is precise: OpenAI « don't bother putting in appropriate attribution of ideas », they « salami-slice 372 results over 719 pdfs », their work « contains retraction-worthy errors », they promise code and fail to include it, and their proofs are « fiendishly hard to parse ». A telling detail: some results had already been found by ChatGPT users writing them up properly, and the bulk release takes the credit for that work away from them. Her thesis fits in the title: not an epistemic catastrophe, just ordinary bad work published without embarrassment.

September 2026: the 25 Fields medallists

The ground had been prepared. On September 11, 2026, 25 Fields medallists — among them Cédric Villani, Pierre-Louis Lions, Hugo Duminil-Copin, Pierre Deligne and Yu Deng — signed a piece in Le Monde titled « A Severe Misalignment of AI in Mathematics ». According to RTBF, they write that announcements arrive « in a rush, without leaving the time needed for rigorous writing-up », and that this « raises serious questions of attribution and plagiarism ».

Their core argument applies to you too: solving a problem is only a means to an end, and the end is understanding. Mass-producing results at a frantic pace risks, they write, destroying fertile ground instead of giving birth to new ideas.

The shock is real. In franceinfo on October 12, Hugo Duminil-Copin, Fields medallist in 2022, speaks of a « monumental shock » and says: « I even cried over it. » Cédric Villani sees « certainly the most radical change in mathematics in at least four centuries ». Ursula Martin, of Oxford, sums up the practical complaint for Nature: the release amounts to tossing the community a messy first draft and expecting it to clean up.

What this changes for you

You are not going to referee a proof about Dirichlet L-functions this term. But five reflexes transfer directly.

A proof that looks right can fall on a sign. What sank three OpenAI manuscripts was not an exotic concept, it was a sign error. When an AI hands you a nicely written solution, the question is not « does this look correct? » but « can I redo every step line by line? ».

Errors propagate. Two proofs fell because they depended on the first. If you build your dissertation on a result you never checked, you inherit its bugs.

« Verified » is not a word, it is a question. Verified by what, against what, covering what share of the work? The gap between 42%, 36% and 24% comes not from a lie but from three definitions of the numerator and the denominator. Faced with any percentage, ask what is being counted.

A preprint is not a peer-reviewed article. None of the 719 documents was refereed before publication. You can cite them, as long as you say what they are. Same rule for the arXiv, HAL or SSRN preprints in your bibliography.

Attribution is the whole story. The central complaint against OpenAI is that it does not cite prior work — exactly what you are asked to do in a dissertation. It is what separates a contribution from a file dump.

One last reflex, whatever tool you use: check your institution's rules on AI before relying on it for graded work, and state honestly what you used.

Our take

Both camps are right about different things, and that is what makes the debate confusing.

On the mathematics, something important happened. Matt Baker, who calls the release sloppy, still writes that « this appears to mark a watershed moment in the history of mathematics ». Dismissing that on principle would be a mistake.

On the method, the criticisms are solid, and they are not even about AI. Failing to cite, slicing one result across several PDFs, promising absent code, publishing 722 documents nobody has reviewed: these are craft failures you would hold against any human author.

What strikes us most is the 42% figure: added two days after release, with a numerator matching no list in the repository, and reprinted as fact by the whole press. A story about mathematical verification whose headline number is itself unverifiable.

For you, the conclusion is simple and a little reassuring. The value is no longer in producing an answer: a machine does that in three hours of compute. It is in the ability to review, to spot a sign error, to say where an idea came from and to explain why something is true. That is precisely what your exams measure.

FAQ

Did OpenAI solve the Riemann hypothesis?

No. The most discussed result concerns the quasi-Riemann hypothesis, a weaker statement. Nature notes that the October 6 batch contains no solution to any of the five remaining Millennium Prize Problems.

Can I cite one of these manuscripts in my dissertation?

Yes, as long as you say what it is: preprints that have not been peer-reviewed, produced by a non-public AI model, some withdrawn or corrected. Cite the version and its date, and flag the status of the document.

What is Lean, concretely?

A proof assistant: software that mechanically checks that a formal proof follows from a formal statement. Highly reliable on that narrow job, but it does not check that the formal statement faithfully translates the natural-language sentence in the paper.

Why do the figures range from 24% to 42%?

Because they count different things: 173 manuscripts out of 719 in the formalization catalogue gives 24%, 135 families out of 372 gives 36%, and OpenAI's 42% refers to « top-line results », a term the repository never defines.

Does this mean AI is bad at maths?

No, and it is rather the opposite that worries mathematicians. The complaint is not about the level of the results, but about how they were published: without attribution, without review, without code.

DEV Community