OpenAI publicerar 719 matematiska manuskript från en outgiven modell: vad Lean har kontrollerat, vad den inte har, och varför matematikerna vill ha kvitton

OpenAI posts 719 maths manuscripts from an unreleased model: what Lean has checked, what it hasn't, and why mathematicians want receipts

On 6 October 2026 OpenAI published Sharing AI progress in mathematics, and the same evening it opened a GitHub repository, openai/math, under the Apache-2.0 licence. The repository holds manuscripts and Lean files produced by what OpenAI calls "an internal frontier model", one it has not released. On the morning of 8 October the README listed 719 manuscripts in 372 families. It said 722 at launch; three were withdrawn on 7 October. According to the README, the model was posed approximately 4,000 problems during the evaluation, and about 42% of top-line results are formalized in Lean. OpenAI's post says the average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking.

The two items drawing the headlines are a claimed proof of the rational Hodge conjecture for CM abelian varieties, a special case rather than the general conjecture, and a claimed zero-free half-plane, Re s > 7/8, for every Dirichlet L-function, the Riemann zeta function included. The repository labels that second result "the quasi-Riemann hypothesis". It is not the Riemann Hypothesis. Both are exactly the results the README lists as exceptions to its standard procedure, and none of these manuscripts has been through peer review. Lean has checked a large slice of the catalogue, not all of it, and a passing check is not the same thing as understanding.

Below: what was released, the two claims in plain language, what Lean settles, what was withdrawn, and what mathematicians are saying. We re-read the repository (GitHub API, README, history file and catalogue), OpenAI's post, Scientific American's 6 October report and the Association for Human Mathematics statement on 8 October 2026.

The post. OpenAI's announcement says the results were "produced by an internal frontier model" and that the company is "working to responsibly release the model that produced these results." It promises "formalizations of many of the proofs in Lean," ten summaries of the model's reasoning and statistics on attempted problems. It also says OpenAI will fund "a series of workshops, conferences, and special programs around the understanding of major results produced by AI." The post itself gives no manuscript or family counts and names neither the Hodge item nor the zeta item. Those details live in the repository.

The repository. GitHub's API shows openai/math was created late on 6 October, Rome time, under Apache-2.0. The README describes "mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model" and says the evaluations were expanded "after performance on our existing mathematical evaluations saturated." Its catalogue had 719 manuscripts in 372 families at the time of writing. A family groups a principal result with companion arguments, consequences or alternative proofs.

Formalization status. The README says "~42% top-line results formalized." The history file gives the arithmetic: 300 of 719. The README is candid about the rest: "Not all have accompanying Lean formalizations," and "Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly."

Procedure. "The vast majority of results were obtained with the same procedure," says the README, which names two exceptions: the zero-free work on the zeta function and the CM Hodge work.

Attention and timing. The repository passed 10,000 GitHub stars by the morning of 8 October, according to the GitHub API. That measures interest, not correctness. Scientific American reports that the repository went public at 6 p.m. EDT on 6 October, which is midnight in Rome.

Hodge, CM case only. In plain terms, drawing on Claire Voisin's 12 September explainer on Terence Tao's blog for background (it predates the release and says nothing about this claim): the Hodge conjecture says that certain cohomology classes on a smooth complex projective variety, the "Hodge classes", are always algebraic, meaning they come from combinations of subvarieties. The general case is one of the Clay Millennium problems and remains open. OpenAI's family 032 in the manuscript map claims the rational Hodge conjecture for CM abelian varieties, a special and highly symmetric family. The README marks this work as outside the standard procedure, and in the repository's catalogue on 8 October it has no Lean formalization.

A zero-free half-plane, not the Riemann Hypothesis. The Riemann Hypothesis says every non-trivial zero of the zeta function lies exactly on the line Re s = 1/2. A zero-free half-plane says something weaker: there are no zeros to the right of some other vertical line. OpenAI's family 003 claims that every Dirichlet L-function, zeta included, has no zeros with Re s > 7/8. The main manuscript is dated 30 September and also covers finite-order Hecke L-functions over Q(√-3). The repository calls this "the quasi-Riemann hypothesis". That is its own label. The claim leaves the whole strip between 1/2 and 7/8 untouched, so it is not the Riemann Hypothesis.

The companion. A second manuscript in the family, dated 5 October, gives an alternative argument for a weaker half-plane, Re s > 11/12. The README says that write-up was human-edited for readability and that the zero-free work sat outside the fixed procedure. The repository's Lean scope note for family 003 covers the 7/8 bound for zeta, for Dirichlet L-functions and for the Hecke case. A formal check of that kind is significant. It is still a claim in a manuscript that has not been peer-reviewed.

What Lean gives you. Lean is a programming language in which a computer checks that a formal statement follows, step by step, from the definitions in a library. Scientific American writes that many of the results "have already been verified in Lean" and "are therefore all but certain to be correct." That is fair as far as it goes. A Lean check does not tell you whether the formal statement matches the English claim in the paper, whether the result is new, or whether the ideas will be useful to anyone. Those remain human jobs. The README also points readers to a Comparator procedure for checking the formal statements themselves.

The split, by OpenAI's own numbers. About 42% of top-line results are formalized, 300 of 719. The rest are prose proofs that, in the README's words, "could have issues." The two headline items sit on different sides of that line: the 7/8 zero-free claim has a Lean entry, and the CM Hodge claim does not, as of 8 October.

Withdrawals within a day. On 7 October the history file recorded that a sign error "invalidates a stabilization-trace cancellation argument" in one manuscript and in two papers that depended on it. OpenAI withdrew all three: "Algebraicity of Weil classes on split abelian eightfolds", "Algebraicity of Kuga–Satake Correspondences for K3 Surfaces" and "The rational Hodge conjecture for products of K3 surfaces". It revised 14 other manuscripts with proof repairs and corrected statements. To be precise: the K3 paper is a different Hodge-related manuscript from the CM claim, which remains in the catalogue. Still, a Hodge-adjacent claim was pulled about a day after release, and the history file is the correction log worth watching.

A reader's habit. When a headline names a famous conjecture, check three things: the exact special case in the repository's own title, whether the family has a Lean entry, and whether the history file shows a withdrawal or revision.

Receipts. Andrew Sutherland of MIT told Scientific American: "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." And: "We should ask for receipts." OpenAI's spokesperson had told the magazine that the model produced almost every result in response to a single prompt handed to a single agent, and that some results might have taken multiple attempts.

Advisory-group norms. Per Scientific American, the independent advisory group of mathematicians announced on 21 September recommends that a company releasing such results make public the model, exact prompt and compute time behind each one. OpenAI is publishing average compute and some statistics, and no prompts. Its spokesperson said the company takes the guidelines seriously but is not bound by them.

Open criticism. The Association for Human Mathematics, in a statement reposted as a guest post on Terence Tao's blog on 7 October, wrote: "Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power." It urged "mathematicians and the public to view the value of this publication model with due skepticism." Scientific American separately notes that Tao has criticised frontier labs for the "insane" pace of their AI-generated results.

The other side. Daniel Litt of the University of Toronto, also to Scientific American: "If we want to know the answers to these math questions, I see no reason why we should ask the company to keep them secret from us." And: "To me, it's going to be a good thing for mathematics."

Who does the checking. OpenAI's spokesperson also told the magazine that many of the newly released results are not yet understood by the company's own mathematicians. Someone has to read 719 manuscripts, and most of that reading will be done by mathematicians who are not paid for it.

---

Where it stands on 8 October 2026. OpenAI's openai/math repository (Apache-2.0) lists 719 manuscripts in 372 families from an unreleased model, down from 722 after three withdrawals on 7 October. About 42% of top-line results are formalized in Lean. The Hodge item is a claim for CM abelian varieties only, with no Lean entry yet. The zero-free item is a Lean-linked claim that every Dirichlet L-function, zeta included, has no zeros with Re s > 7/8. The repository calls it the quasi-Riemann hypothesis; it is not the Riemann Hypothesis, which concerns the line Re s = 1/2. None of the manuscripts has been peer-reviewed.

The catalogue count has already moved once. Before you cite a number, check the README and the history file.