October 10, 2026 ·33 min read·中文版

After Seven Hundred Manuscripts: A Meta-Analysis of OpenAI's Mathematical Results, and Seventy Years of Machine Proof

If confirmed, some of these manuscripts would be among the most important mathematical advances in decades; at the time of writing, none has been peer reviewed. This piece doesn't judge whether the proofs are right. It answers three checkable questions: what exactly was released, where the problems come from, and how we got here.

science

At around 3 p.m. Pacific time on 6 October 2026, a new repository called openai/math appeared on GitHub. It had a single commit, its author field read “Anonymous”, and it contained 722 mathematical manuscripts, a library of Lean formal proofs, and ten excerpts of the model’s reasoning (repository README[1]). A few dozen minutes later OpenAI published a blog post and social-media posts calling it “a batch of new mathematical results produced by an internal frontier model” (OpenAI blog[2]).

The titles in the catalogue read like a wish list for mathematics: a quasi-Riemann hypothesis, Hilbert’s tenth problem over the rationals, the irrationality of Catalan’s constant, the irrationality exponent of π equal to 2, the Unique Games Conjecture, several of Kaplansky’s group-ring conjectures, Mahler’s conjecture… That evening Alex Kontorovich of Rutgers wrote on X: “If a human had done this, it would be an uncontested Fields Medal.” (original post[3], as quoted in the press). Among the same mathematicians, others called it “a display of power, not of scholarship”.

This piece sets out to do three things. First, to restate as accurately as possible what the release actually contains, what OpenAI said about it and what it didn’t say. Second, to carry out a meta-analysis of the 372 result families: which disciplines they fall in, whether the conclusions are proofs, refutations or partial progress, in what year the original problem was posed, and how many come with formal proofs. Third, to place the event in the history of machine proof and ask in what senses it is new.

First, a note on stance and limits. This piece does not assess whether any particular proof is correct; that is beyond any survey, and beyond any single person at present. Wherever OpenAI says something, it is written as a “claim”; wherever the classifications and inferences are our own, the basis is stated.

1. What the release contains

Scale and definitions

According to the repository README and the catalogue file overview.tex, the material has three levels. At the bottom are 722 manuscripts, each a separate PDF with its LaTeX source; these are grouped into 372 “result families”, each containing one main result plus its supporting arguments, corollaries or alternative proofs; and the result families are in turn sorted into 17 disciplines. The families are numbered 001 to 377, with five numbers — 045, 061, 070, 123 and 163 — unused, so the “377 problems” in some reports is the highest number, not the count.

On how the results were produced, the README says only a few things:

The results were produced by “an unreleased internal OpenAI model”; the model’s name was not given.
During evaluation the model was “posed roughly 4,000 problems”; OpenAI aggregated the outputs into result families and manuscripts, “requiring an appropriate level of significance”, to arrive at this catalogue.
On average, each result used “compute equivalent to three hours of ChatGPT Pro thinking”.
Two pieces of work fall outside this fixed pipeline: a zero-free region for the Riemann zeta function, and the Hodge conjecture for CM abelian varieties; the zero-free-region manuscript for Re(s) > 11/12 “was edited by humans for readability”.
The README explicitly warns: “some unformalised results may contain problems.”

Two points deserve attention. First, “4,000 problems” and “372 result families” cannot simply be divided to give a “success rate”: OpenAI has published neither the per-problem attempts and outcomes nor how the “significance threshold” was set. Scott Aaronson’s blog gives about 8,000 problems and a success rate of about 5% (Shtetl-Optimized[4]), which is inconsistent with the README; we follow the README. Second, “three hours of ChatGPT Pro thinking” is a product-level unit of measure that doesn’t correspond to comparable GPU hours or cost; total compute and cost were not disclosed.

We counted the pages of all 722 PDFs: 34,815 pages in total, with a median of 39 pages per manuscript, the shortest 6 and the longest 262. By result family, the median is 56 pages, and the longest family (the spacetime Penrose inequality, number 260) runs to 1,355 pages. The dates in the manuscript directory names run from 10 September to 6 October 2026, with 564 manuscripts concentrated in the five days from 23 to 27 September.

What it claims to have solved

Listing all 372 results would serve no purpose. Here are just a few of the claims that have drawn the most attention and whose weight is easiest for non-specialists to grasp, worded as closely as possible to the catalogue:

A quasi-Riemann hypothesis (number 003): no Dirichlet L-function, including ζ(s), has a zero in the half-plane Re s > 7/8. All currently known zero-free regions shrink towards the line Re s = 1 as the imaginary part grows; any fixed θ < 1 is an open problem.
Hilbert’s tenth problem over the rationals (004): there is no algorithm to decide whether an arbitrary multivariate polynomial with integer coefficients has a rational zero.
Catalan’s constant is irrational (005); the irrationality exponent of π is 2 (017).
The Unique Games Conjecture (102): the computational-complexity conjecture Khot posed in 2002, which the catalogue says it “proves”.
The matrix multiplication exponent ω ≤ 9/4 (107). The previous best upper bound was about 2.371.
Counterexamples to Kaplansky’s zero-divisor conjecture (196) and the direct-finiteness conjecture (197), the latter also constructing a non-sofic group.
The free group factor isomorphism problem (287): L(F₂) ≅ L(F₃), a question open in operator algebras for decades.
Thompson’s group F is non-amenable (248); a counterexample to Hadwiger’s conjecture (157); Mahler’s conjecture (087).

Result families and “claims”: this piece calls each numbered entry in OpenAI’s catalogue a “result family”. The catalogue summarises each family’s main conclusion in a sentence or two; these summaries are OpenAI’s own statements. As of 8 October 2026 we found no result family that had been through journal peer review, and no public report identifying an error in any of them.

Lean formalisation: what is proved and what isn’t

What most distinguishes this release from every earlier announcement of “AI solves maths problems” is that it comes with a very large Lean formalisation library. The repository’s lean/OAI directory holds about 120,000 Lean source files, 1.7 GB of code, using Lean 4.34.1 and mathlib and depending on more than twenty external formalisation projects.

Lean and Comparator: Lean is an interactive theorem prover: mathematical statements are written as formal propositions and proofs as programs, and a very small “kernel” checks step by step that every inference is valid. Comparator is a verification tool developed by the Lean community: given a “challenge file” that contains only the statement, with the proof left as sorry, it checks that a compiled solution proves exactly that statement and uses only the permitted axioms (usually the three standard ones, propext, Quot.sound and Classical.choice).

Concretely, lean/docs contains formalisation scope notes for 235 result families, 63% of the 372; the manifest formalization.yaml lists 162 manuscripts whose “main results are formalised” and Comparator configurations for 185 main results; and the ComparatorChallenges directory holds 405 challenge configurations in all. The three numbers measure different things and cannot stand in for one another. There is also an inconsistency: Catalan’s constant (005) and the irrationality exponent of π (017) both have scope notes and challenge files but are not on the formalization.yaml list.

More important are two qualifications. First, the manifest’s overall status is marked scope: "Partial progress." and its review status review: status: unchecked. Second, the scope notes themselves often spell out the limits of what is formalised: the one for π says “the paper’s corollary on the convergence of the Flint–Hills series is not within this statement”, and the one for the quasi-Riemann hypothesis says “the paper’s subsequent applications are not included”.

A further boundary in principle has to be stressed: Lean can only guarantee that “this code proves this formal statement”, not that the formal statement is the conjecture mathematicians have in mind. Take the quasi-Riemann hypothesis: the statement in the challenge file is

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0

Here riemannZeta is an existing mathlib definition, and the statement is short enough for anyone who has studied complex analysis to read, so whether the statement is faithful is barely an issue in this case. But for statements like the Unique Games Conjecture, the formal statement itself is hundreds of lines of definitions, and checking its faithfulness requires an expert to read it line by line.

2. Meta-analysis: 372 result families

Method

The data come directly from the repository’s catalogue file overview.tex (commit adc7f12). A script parsed out each result family’s number, discipline, title, catalogue summary, manuscripts and dates; we checked whether lean/docs contains a corresponding scope note, and used pdfinfo to count the pages of each PDF.

On that basis, we read each result family by hand and recorded three things:

Original problem: which named conjecture, problem or question it addresses, and who posed it.
Year posed: the year the problem first appeared in the literature or was publicly posed — not the year of later partial progress. Where this couldn’t be determined reliably, we left it blank rather than guess.
Type of conclusion: five categories. “Claimed full solution” means a complete affirmative answer to the original problem; “negative or counterexample” covers constructing counterexamples and negative answers to decision problems; “partial progress” means special cases, conditional results or partial parameter ranges; “improved bound” means improving a quantitative upper or lower bound without reaching the conjecture itself; “other” means new theorems not framed as solving an existing problem.

The reading was done in six batches, mainly from the mathematical literature and surveys, consulting original papers, erdosproblems.com, arXiv and encyclopaedia pages for uncertain entries. Afterwards, we drew 40 dated entries at random and had an independent second pass re-establish their years; all 40 matched the first pass. About ten of these were checked against original sources or authoritative pages online; the rest relied on the checker’s knowledge of the original literature. This shows the years are broadly reliable, but not that every one is exact to the year. The full data table accompanies the article in its directory and can be checked entry by entry.

A few definitional points need stating in advance. A result family often deals with several related problems; we take the primary problem in the catalogue title. “Type of conclusion” is based on OpenAI’s catalogue summary — that is, its claimed conclusion — and does not mean we think the conclusion holds. The line between “partial progress” and “claimed full solution” sometimes depends on the reader; for example, a family that resolves all remaining cases of a conjecture is recorded as a full solution.

Disciplines: almost all of modern mathematics

Figure 1 | 372 result families by discipline and type of conclusion. Disciplines follow OpenAI's catalogue; conclusion types were judged family by family by 一目半 (Yimuban) · Source: openai/math repository catalogue (commit adc7f12), compiled and drawn by 一目半

The five disciplines with the most result families are theoretical computer science (40), combinatorics (37), algebraic and complex geometry (36), number theory (31), and probability and statistical mechanics and differential geometry (29 each); the fewest is mathematical logic (6). None of the 17 disciplines has fewer than 6 result families — a contrast with most earlier “AI does maths” results, which were concentrated in combinatorics and discrete mathematics.

By type of conclusion, 217 result families (58%) claim a full solution of the original problem, 74 (20%) are negative results or counterexamples, 53 (14%) are partial progress, 18 (5%) are improved bounds, and 10 (3%) are other new results.

One notable pattern is that the share of counterexamples varies greatly between disciplines. In algebra, 8 of 18 result families are counterexamples; in topology 6 of 18; in operator algebras 6 of 19. In number theory, only 1 of 31; in probability and statistical mechanics, none of 29. One possible explanation: algebra and topology have many conjectures of the form “do all objects of a certain kind have a certain property?”, which a single constructed object can refute — and construction is exactly what search-based systems are good at; the core problems of number theory and probability are more often asymptotic estimates and limit theorems, which are hard to overturn with one example. This is an inference and has not been tested.

When the problems were posed: mostly between the 1960s and 2000s

Figure 2 | The 283 datable result families by the decade the original problem was first posed; axis labels give the first year of each decade. Lighter bars: before 1950 · Source: openai/math repository catalogue, dated entry by entry and drawn by 一目半 (Yimuban)

Of the 372 result families, 363 correspond to a named existing problem, of which 283 can be reliably dated. Another 80 have names but are mathematical “folklore problems” that are hard to trace to a single first statement — the quasi-Riemann hypothesis, or whether Catalan’s constant is irrational, for example; and 9 address no existing problem.

Of the 283 datable families:

The median is 1986, with quartiles of 1971 and 2004 — that is, half the problems were posed between 1971 and 2004.
158, or 56%, were posed between 1960 and 1999; the peak is the 1970s (52).
97 were posed at least 50 years ago; 24 before 1950, the earliest being Schläfli’s 1873 question on local smooth isometric embedding of surfaces, along with forms related to problems 5, 6 and 16 on Hilbert’s 1900 list.
42 were posed from 2010 on, and only 8 from 2020 on.

We also flagged “famous problems” — conjectures widely known outside their own field, usually with their own encyclopaedia entry — 75 in all. This flag is partly subjective and only indicative. Of these 75, 38 claim a full solution and 23 are negative results or counterexamples; the median year of the datable ones is 1971, 15 years earlier than the whole set.

How to read this distribution? One direct observation is that these problems are neither recently posed ones that haven’t been seriously attempted, nor mainly century-old challenges, but cluster in the range of “a mature literature, a clear statement, attempted by a generation or two”. This echoes the selection criterion OpenAI used for the ten “Astra” results in August, which was “no progress on the main result for at least ten years” (OpenAI[5]). But the README doesn’t disclose where this batch of problems came from, so we can’t tell whether the distribution reflects the limits of the model’s ability or the preferences of whoever chose the problems.

In addition, 17 result families concern problems posed by Erdős. Compared with the run of stories about AI and Erdős problems since the second half of 2025, this release’s centre of gravity is clearly elsewhere.

Formal coverage: closely tracking the maturity of mathlib

Figure 3 | Share of result families in each discipline with a Lean formalisation scope note; the dashed line is the overall average of 63%. A scope note does not mean the main theorem is fully formalised · Source: openai/math repository lean/docs and catalogue, compiled and drawn by 一目半 (Yimuban)

235 result families come with a Lean scope note, but disciplines differ widely: mathematical logic 6/6, functional analysis 10/11, combinatorics 33/37, convex and metric geometry 13/15, group theory 12/14; while number theory has only 16/31, algebraic and complex geometry 7/36 (19%), and topology 3/18 (17%).

By type of conclusion, 17 of the 18 improved bounds have notes, negative results or counterexamples 53/74 (72%), claimed full solutions 141/217 (65%), and partial progress only 18/53 (34%).

A reasonable guess is that formal coverage depends mainly on how complete the relevant theory is in mathlib: combinatorics, logic, and elementary analysis and geometry already have extensive infrastructure, while the tools algebraic geometry and geometric topology need — schemes, cohomology, the topology of manifolds — are still incomplete in Lean. Counterexamples and quantitative bounds may have high coverage because they often only require checking one concrete construction, and the statements themselves are easier to formalise. This, too, is an inference.

It has a practical consequence: in this batch, precisely the part the mathematical community will find hardest to review independently — the long arguments in algebraic geometry and the Langlands programme, for example — has the least machine verification behind it. The Hodge conjecture for CM abelian varieties (032), modularity of elliptic curves over imaginary quadratic fields (030) and Hilbert’s tenth problem over the rationals (004), for instance, have no formalisation notes.

Independent verification

As of 8 October, the only independent verification we could find covers the single 7/8 statement of the quasi-Riemann hypothesis. The developer Dave Goldblatt re-ran this theorem through Comparator on one machine, reporting that it passed both under OpenAI’s configuration and under a challenge file he wrote himself, using only the three standard axioms (davegoldblatt/openai-zeta-proof-check[6]). He also listed limitations: he checked only the Lean proof, not the paper; he applied 23 patches to dependencies during the build; and 402 of OpenAI’s 405 challenge configurations turn off Comparator’s second kernel check. Another project reported completing the build and the axiom check but did not run Comparator.

We also carried out a small check of our own. The target was result family 049, which claims to refute the hypersurface form of the Abhyankar–Sathaye conjecture in dimension four and above. The conjecture predicts that if the quotient ring ℂ[x₁,…,xₙ]/(F) of a polynomial F is isomorphic to a polynomial ring in n−1 variables, then F must be a coordinate — that is, it can be turned into one of the variables xᵢ by a polynomial automorphism. We chose it for two reasons: it is a long-standing open problem in affine algebraic geometry, and its formal proof is small — depending only on mathlib and 15 source files, about 1,400 lines — so it can be rebuilt completely from source on an ordinary machine.

In a fresh Lean 4.34.1 project, we compiled all dependencies from source at the mathlib version pinned by the repository (1,626 build jobs, about 17 minutes on 4 cores), then ran three checks:

We copied the statement from the challenge file verbatim into an example and proved it with OpenAI’s theorem; it compiled. This shows that what is proved is indeed the statement written in the challenge file.
We used #print axioms to check which axioms the theorem depends on: only the three standard axioms, propext, Classical.choice and Quot.sound — no sorryAx and no extra axioms.
We used Lean’s own independent checker, leanchecker --fresh, to replay the module and all its dependencies (including the parts of mathlib it uses) through the kernel from scratch; after about 5 minutes it passed with no errors. This further rules out the possibility that faulty or tampered intermediate build files affected the result.

This check shows one thing only: result family 049’s Lean proof holds, in the sense of its formal statement. Whether the statement accurately expresses the Abhyankar–Sathaye conjecture is for algebraic geometers to judge; from how the statement is written, it uses mathlib’s standard definitions and its meaning is quite direct. It cannot be extended to the other 371 result families.

3. How mathematicians reacted

At the time of writing, reactions fall roughly into three groups.

The first is astonishment at the results themselves. Besides Kontorovich, Steven Strogatz of Cornell wrote that “there are a lot of astonishing results here”, and Paata Ivanisvili of UC Irvine wrote that “three-dimensional Kakeya won a Fields Medal; four-dimensional Kakeya was solved by AI”. To be precise, what the catalogue claims is the three-dimensional Kakeya maximal function conjecture and the four-dimensional Hausdorff dimension conjecture, not the whole Kakeya conjecture. The number theorist Frank Calegari had posted a set of open problems from his own field earlier on the day of the release; afterwards he updated it to say that, scored against his list, it was only “5/100”, “but on the other hand still jaw-dropping” (Persiflage[7]).

The second is concern about readability and understanding. Scott Aaronson wrote that, for the Unique Games Conjecture, “we’re fairly confident it’s a proof”, but also that “almost no one has yet really understood any of these proofs”; he relayed Dana Moshkovitz’s assessment that the paper is painful to read, “almost unreadable without the help of AI” (Shtetl-Optimized[4]). According to Scientific American, an OpenAI spokesperson also acknowledged that the company’s own mathematicians don’t yet understand many of the results; MIT’s Andrew Sutherland’s position is that until the model is public and others can reproduce the work, “we should ask for receipts”. These two are relayed from secondary reports; we could not open the originals directly.

The third is criticism of the manner of release itself. A group calling itself the Association for Human Mathematics published a statement on Terence Tao’s blog, saying that “releasing more than 700 documents at once is a display not of scholarship but of power” (guest statement on Tao’s blog[8]). Before the release, the Advisory Group on Mathematics and AI (AGMAI), hosted by the Institute for Advanced Study in Princeton, had recommended on 29 September that AI companies disclose prompts, models and per-problem compute, and stop testing advanced mathematical problems on proprietary models; this time OpenAI disclosed no prompts and released no model. After the release, the group said it was “a big event for mathematics”, but that its advisory role “should not be read as a judgement on the impact of these results” (AGMAI[9]). Nature’s news headline was “Mathematicians in uproar” (Nature[10]).

These reactions are not contradictory. The same person can quite reasonably find the results astonishing and the manner of release harmful. It is worth recording that, as of 8 October, we found no public assessment of specific results by Tao, Gowers, Buzzard, Scholze and others; this only means we didn’t find any, not that they haven’t spoken. The repository still has only its one initial commit, with no record of corrections, and its Issues feature is switched off.

Lean answers “is there an error in this reasoning?”; peer review answers “is this worth it, and do we understand it?” This release is the first time the answer to the first question has come far faster than the answer to the second.

4. Machines and proof: a seventy-year timeline

Figure 4 | Key moments in machines' participation in mathematical proof, 1956–2026. Dates are when events were announced or completed; most 2026 results have not been peer reviewed · Source: original papers and official announcements for each event, compiled and drawn by 一目半 (Yimuban)

Beginnings: turning logic into programs (1956–1970s)

Machine proof was born almost at the same moment as the phrase “artificial intelligence”. In 1956 the Logic Theorist of Allen Newell, Herbert Simon and Cliff Shaw proved 38 of the first 52 theorems in chapter 2 of Whitehead and Russell’s Principia Mathematica, one of them with a shorter proof than the book’s (Newell & Simon 1956, IRE Trans. Inf. Theory[11]). The Logic Theorist imitated human heuristic search. Two or three years later, Hao Wang took another route: using systematic decision procedures on an IBM 704, he proved hundreds of propositions from Principia in minutes, including all 52 the Logic Theorist had handled, and argued on that basis that mechanical methods were far more effective than imitating humans (Wang 1960, IBM J. Res. Dev.[12]).

The split between these two routes — heuristic search that imitates human intuition, and systematic formal reasoning — runs through the next seventy years. In 1965 J. A. Robinson proposed the resolution principle, giving a unified method for automated proof in first-order logic (Robinson 1965, J. ACM[13]). In 1967 N. G. de Bruijn launched the Automath project, one of the first languages for writing mathematical proofs that a machine could check; ten years later L. S. van Benthem Jutting used it to verify the whole of Landau’s Foundations of Analysis (Automath archive[14]).

Computer-assisted proof and the “checkability” debate (1976–2017)

In 1976 Kenneth Appel and Wolfgang Haken announced a proof of the four colour theorem. The key step had a computer check nearly two thousand reducible configurations, which no human could re-check one by one. This was the first time the proof of an important theorem could not be read in full by a person, and mathematicians argued: is a proof no one can read through really a proof?

Later milestones answered the question in different ways. In 1996 William McCune’s automated prover EQP proved the Robbins conjecture, posed in 1933 — a famous open problem solved independently by an automated theorem prover (McCune 1997[15]). In 1998 Thomas Hales announced a proof of the Kepler conjecture using extensive computation; after years of review, the referees for Annals of Mathematics said they were “99% certain” but could not check all the computations. Hales then launched the Flyspeck project to formalise the entire proof in the proof assistants HOL Light and Isabelle; it was completed in 2014 and published in 2017 (Hales et al. 2017, Forum Math. Pi[16]).

In the same period, Georges Gonthier and colleagues used Coq to complete formal proofs of the four colour theorem (2005) and the Feit–Thompson odd order theorem (2012) (Gonthier 2008, Notices AMS[17]). The answer these works gave: a proof in which machines take part can be re-checked by another machine with very high confidence, and the checker need only trust a small kernel.

Proof assistants enter mainstream mathematics (2013–2024)

Leonardo de Moura began developing Lean at Microsoft Research in 2013, and the community library mathlib was built up from 2017. The turning point came in December 2020, when Peter Scholze publicly challenged the formalisation community to verify a theorem from his and Dustin Clausen’s condensed mathematics that he himself wasn’t fully confident about. This “Liquid Tensor Experiment” was completed in July 2022 (Xena blog[18]). In November 2023 Gowers, Green, Manners and Tao proved the polynomial Freiman–Ruzsa conjecture, and the community formalised it in about three weeks (PFR project[19]). By 2024, the Equational Theories Project organised by Tao, combining automated provers, people and Lean, had settled more than 22 million implications between 4,694 magma laws.

The significance of this phase: formal proof stopped being just a tool for computer scientists and became infrastructure that working mathematicians were willing to use and to trust. It is this infrastructure that lets today’s large-model output be checked by machine.

Neural networks and large language models (2020–2025)

In September 2020, OpenAI’s GPT-f used a language model to generate proofs for Metamath, 23 of which were formally accepted into the main Metamath library (Polu & Sutskever 2020[20]). In December 2021, DeepMind and mathematicians from Oxford and Sydney published a collaboration in Nature that used machine learning to find new relations between knot invariants and advanced the combinatorial invariance conjecture for Kazhdan–Lusztig polynomials (Davies et al. 2021, Nature[21]). Later, AlphaTensor (2022) and FunSearch (2023) used search to find new matrix multiplication algorithms and larger cap-set constructions.

Competition mathematics became the most conspicuous yardstick of this phase. In January 2024, AlphaGeometry solved 25 of 30 IMO geometry problems (Trinh et al. 2024, Nature[22]); that July, AlphaProof and AlphaGeometry 2 scored 28/42 at IMO 2024, silver-medal level, though the problems had to be translated into Lean by hand and some took three days. In July 2025, OpenAI’s experimental model and Google’s Gemini Deep Think both reached the gold-medal line of 35/42 at IMO 2025 with natural-language answers, the latter graded by IMO officials; Harmonic’s Aristotle and ByteDance’s Seed-Prover gave Lean-formalised solutions to five problems.

Research-level evaluations followed. In November 2024 Epoch AI released FrontierMath, on which the best model at the time solved under 2% (Glazer et al. 2024[23]). In May 2025 DeepMind’s AlphaEvolve found an algorithm to multiply 4×4 complex matrices with 48 multiplications, improving on the 49 that had stood since Strassen in 1969.

October 2025 brought a mistake worth remembering. An OpenAI vice-president posted that GPT-5 had “found solutions to 10 previously unsolved Erdős problems”; Thomas Bloom, who maintains the Erdős problems website, promptly called this “dramatically misleading”: the problems were marked “open” on the site only because he personally didn’t know of existing solutions, and what GPT-5 had found was existing literature. The post was later deleted (TechCrunch[24]). In the months that followed, real progress on Erdős problems with substantial AI involvement did appear: in December 2025, for instance, problem 1026 was solved through a collaboration of Aristotle, AlphaEvolve, literature search and several mathematicians, with Tao documenting the process in detail (Tao’s blog[25]). Tao and others then maintained a wiki of “AI contributions to Erdős problems”, recording each case by category — full, partial, incorrect, literature found only, and so on (GitHub wiki[26]). That classification is one of the reference points for this piece’s meta-analysis.

2026: from one-off breakthroughs to batch production

The pace picked up markedly in 2026. In chronological order, these are the events directly relevant here.

February: Abouzaid, Hairer, Srivastava and eight other mathematicians released “First Proof”, testing AI on 10 unpublished research-level problems (arXiv:2602.05192[27]). OpenAI claimed at least 5 were “likely correct”, while acknowledging human guidance (OpenAI[28]); a majority of experts judged that DeepMind’s Aletheia had solved 6 (arXiv:2602.21201[29]).
20 May: OpenAI announced that its internal model had refuted Erdős’s 1946 unit-distance conjecture — that is, proved there are infinitely many n for which n points in the plane can have at least n^(1+δ) pairs at unit distance. The result was checked by a group of outside mathematicians; Gowers called it “a milestone for AI mathematics”, and Jacob Tsimerman said he would accept it for publication “without hesitation” (OpenAI[30]).
2 June: a group of mathematicians published the Leiden Declaration, endorsed by the International Mathematical Union, stressing that AI is a tool and not an author, and listing five kinds of risk: unreliability, authorship, proprietary dependence, hype and autonomy (Leiden Declaration[31]).
19 July: Levent Alpöge, a researcher at Anthropic, published a counterexample to the three-dimensional Jacobian conjecture, posed by Keller in 1939. The counterexample is a degree-7 polynomial map that can be verified directly with computer algebra. Alpöge credited it on social media to Anthropic’s model; Shuhong Gao then extended the construction to every dimension greater than 2 (arXiv:2608.00222[32]). The two-dimensional case remains open.
August: OpenAI released ten “Astra” results, each with a Lean certificate (OpenAI[5]). Anthropic announced that its unreleased model had raised the proven lower bound on the proportion of ζ zeros on the critical line from 41.6% to 67.2%, with a Lean proof, and stated explicitly that this has nothing to do with proving the Riemann hypothesis (Anthropic[33]).
8 September: OpenAI claimed its multi-agent system had proved the “blow-up” direction of the Clay Millennium Problem on the Navier–Stokes equations — finite-time blow-up with smooth forcing — with a Lean formalisation, and said it would not claim the prize (OpenAI[34]). The Clay Institute has not yet ruled, and the episode has come with a priority dispute involving Alpöge and Tristan Buckmaster.
11 September: 28 Fields Medallists signed “The Serious Misalignment of AI in Mathematics”, criticising AI companies for treating mathematical problems as benchmarks, with results “announced in haste, before proper manuscripts can be written”, and for raising “serious problems of attribution and plagiarism” (mathandai.org[35]).
Late September: the Institute for Advanced Study in Princeton set up the independent Advisory Group on Mathematics and AI (AGMAI), with nine members including Gowers, Hairer and Witten; one of its first tasks after being set up was to advise on this large-scale OpenAI release.
6 October: the 722 manuscripts discussed here were released.

We apply the same standard to every company’s announcements above: we state only what was announced and what is known of external checking.

5. Some reflections

The production, verification and understanding of proofs are coming apart

In the past, proving, verifying and understanding a theorem were usually done by the same group of people in the same process: the prover wrote the argument, referees read and confirmed it, and colleagues absorbed its ideas as they read. The four colour theorem was the first to partly detach “verification” from this process and hand it to a machine; formal mathematics made that detachment trustworthy.

This release pushes the detachment into the third stage. Even at 20 pages a day of careful reading by one expert, 34,815 pages would take nearly 1,750 working days. More crucially, Aaronson’s and Moshkovitz’s comments suggest that even when a proof is right, its ideas may not be readily absorbed by humans. This raises a question that used to appear only in philosophical discussions: if a theorem is proved by a machine and verified by a machine but understood by no one, in what sense has it become mathematical knowledge?

The verification bottleneck has moved to “is the statement faithful?”

Lean makes the question “is there an error in the proof?” mechanically answerable, but it moves the pressure elsewhere: does the formal statement accurately express the original conjecture? For a short statement like the quasi-Riemann hypothesis this is easy to check; for statements like the Unique Games Conjecture or the Hodge conjecture, which need many definitions to state, reviewing the formal statement is itself specialist work. Moreover, as noted above, the disciplines most in need of machine verification are precisely those where the formalisation infrastructure is weakest.

Norms are lagging behind capabilities

From the Leiden Declaration and the Fields Medallists’ statement to AGMAI’s guidance, the mathematical community put great effort in 2026 into discussing norms: attribution, disclosure, reproducibility, pace. This release responds to some of them formally — consulting AGMAI, attaching formal proofs, promising to keep version history — but did not take the advice on prompts, model availability and pace of release. A foreseeable consequence is that over the next few months many mathematicians will be forced to shift from “proving new theorems” to “reviewing AI’s theorems”, and that labour currently has no clear credit or reward.

For readers working where AI meets the life sciences

Many readers of this column work where AI meets the life sciences. Mathematics is the field where AI can most easily “verify itself”: it has a rigorous formal language and proofs that can be checked mechanically. Even so, the problems this release exposes — uneven verification coverage, statement faithfulness, human understanding falling behind, a pace of release that overwhelms review capacity — are real in mathematics. Biology has neither Lean nor a small kernel that can guarantee a conclusion is correct, and experimental verification is slow and expensive. It is reasonable to expect that when AI starts producing “discoveries” in bulk in biology, these problems will only be worse. The norms mathematics established in 2026 may be worth the life sciences borrowing ahead of time.

Conclusion, and questions still open

Back to the start. What OpenAI released is 372 result families and 722 manuscripts, selected after an internal model was run on roughly 4,000 problems. By our tally, 58% claim a full solution of the original problem and 20% give a refutation or counterexample; the median year in which the original problems were posed is 1986, concentrated between 1971 and 2004; 63% of the result families come with Lean formalisation notes, but coverage is high in combinatorics and logic and low in algebraic geometry and topology. As of 8 October, no result has been through peer review, and none has been shown to be wrong.

This survey has some limitations. First, the conclusion types are based on OpenAI’s catalogue summaries and do not mean the conclusions hold. Second, the years in which problems were posed rest mainly on the literature and our reading; the sampled check agreed, but individual entries may be off by a few years, and 89 result families could not be dated reliably. Third, the “famous problem” flag is partly subjective. Fourth, we can only see the results that were selected and published, not what happened on the other roughly 3,600 problems, so none of the proportions here can be read as the model’s success rate.

Key points

On 6 October 2026, OpenAI released 722 mathematical manuscripts in 372 result families, produced by an unnamed internal model on roughly 4,000 problems, using on average about the equivalent of three hours of ChatGPT Pro thinking per result; the manuscripts total 34,815 pages.
By 一目半’s family-by-family tally: 58% claim a full solution of the original problem and 20% are refutations or counterexamples; the 283 datable problems have a median year of 1986, with 24 posed before 1950; counterexamples are most common in algebra, topology and operator algebras, and almost absent in number theory and probability.
63% of the result families come with Lean formalisation notes, but the repository’s overall status is “partial progress, unchecked”, and coverage is lowest in algebraic geometry and topology; as of 8 October, independent formal re-checks cover very few statements, and no result has been peer reviewed.
From the Logic Theorist in 1956 to the batch release of 2026, machines first took over search and then verification; this release shows that proofs are now being produced far faster than humans can understand and review them.

At least three questions remain open. First, how many of these results will be confirmed on close reading, and how many will need correcting? OpenAI has promised to record corrections, which will be the first real data on its reliability. Second, when a proof has been verified by machine but understood by no one, how should the mathematical community treat it — accept it, cite it, or wait for a human-readable version? Third, will the choice of problems itself change: once “problems posed decades ago with clear statements” can be solved in bulk, will mathematicians shift their energy to posing problems, building theories and explaining results? The answers will probably only become clear over the next year or two.

Data and method note: the full data table for this meta-analysis is openai-math-families.csv in the article’s directory, one row per result family, with fields for discipline, title, original problem, proposer, year posed and its basis, confidence in the year, type of conclusion, whether it is an Erdős problem, whether it is a famous problem, number of manuscripts and total pages, manuscript date range, whether it has a Lean scope note, the result of the sampled re-check, and OpenAI’s original catalogue summary. The data come from commit adc7f1241b42e322a6451854ab7e4b4c146bf78a of the openai/math[1] repository. All charts were drawn by 一目半 (Yimuban) from these data.