OpenAI publishes hundreds of machine-written maths proofs - and pulls three within a day

FACT. On 2026-10-06, OpenAI published a research post titled "Sharing AI progress in mathematics" and released a public GitHub repository, openai/math, containing mathematical manuscripts and supporting proof artifacts produced by an unreleased internal OpenAI model.

FACT. The repository's README states the catalogue contains 719 manuscripts organised into 372 result families, with a preprints/ directory (PDFs, source files, citation/build instructions), a lean/ library and formalization catalogue, a reasoning_traces/ directory, and CONTENTS.md, overview.pdf, history.md. The repository is released under an Apache-2.0 licence. (Note a count discrepancy: OpenAI's post does not give a number; the README states 719 manuscripts; multiple outlets — Retraction Watch, Unite.AI, The Decoder — report 722 manuscripts. See Limitations.)

FACT. OpenAI's post states it is "releasing a broad range of new mathematical results produced by an internal frontier model," that it is sharing formalizations of many proofs in Lean, and that it is publishing 10 abridged summaries of the model's reasoning, estimates of compute "in terms of Pro usage on ChatGPT," and statistics on the number of problems attempted. It states the average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking.

FACT. The repository README states that over the evaluation the model was posed approximately 4,000 problems, and that the average result used three hours of ChatGPT Pro thinking compute with that model. It states the repository has "~42% top-line results formalized" (300/719).

FACT. OpenAI states it consulted the independent Advisory Group on Mathematics and Artificial Intelligence (AGMAI) at the Institute for Advanced Study and drew on its advice and public recommendations. AGMAI published general recommendations on 2026-09-29 and a statement specifically on OpenAI's release on 2026-10-06.

FACT. On 2026-10-07, the repository's history.md recorded the withdrawal of three manuscripts — "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" — because "a sign error invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers." The same entry records revisions to 14 other manuscripts and adds that formalization now covers 300/719 ≈ 42%.

FACT. Named exceptions to OpenAI's fixed procedure, per the README: work on a zero-free region for the Riemann zeta function and a proof of the Hodge Conjecture for CM abelian varieties; the write-up for the Re(s) > 11/12 zero-free region was human edited for readability.

COMPANY CLAIM. OpenAI's framing that this release "pushes the frontier of human knowledge and enables further progress in mathematics," that the results solve or advance hundreds of open questions, and that the compute-per-result figures characterise the model's capability.

INDEPENDENT EVIDENCE. Independent mathematical and scientific media (Quanta, Scientific American, Retraction Watch) and independent mathematicians (Sutherland, Townsend, Moshkovitz, Tao, Gowers, Aaronson) confirm the release happened, that the manuscripts are public, and that the field considers it a major event — while disputing how much of it should be treated as established mathematics and criticising the release process.

FACT. Before 2026-10-06, OpenAI's major 2026 mathematics disclosures were announcements of specific results (the 2026-09-08 Navier–Stokes post and the 2026-09-21 advisory-group announcement). On 2026-10-06 the mode of disclosure changed to a bulk, self-hosted, versioned public repository with generated proof artifacts and reasoning summaries.

FACT. Measurement and review infrastructure changed: results now ship with Lean formalizations for a stated ~42% of top-line results, a machine-readable formalization catalogue, citation blocks per manuscript, a revision/withdrawal log, and published compute estimates — a materially richer disclosure than a press announcement alone, though below AGMAI's recommendations (no prompts, no per-result compute).

INTERPRETATION. The unit of AI mathematics output shifted from "a breakthrough announcement" to "a corpus with a changelog." Release engineering, attribution, versioning and external digestibility became first-order concerns rather than afterthoughts. It also shifted the bottleneck: the limiting factor is no longer problem-solving but human understanding, exposition and verification capacity.

INTERPRETATION. The event re-framed whose responsibility verification is. OpenAI published unverified material and invited the community to check it; AGMAI called publication "a first step"; AHM rejected the framing and called it "a demonstration of power." The default expectation that an author understands and vouches for their own proof was explicitly suspended for roughly half the corpus (OpenAI's spokesperson described roughly 50% as released unconfirmed).

Before.

• AI mathematics progress was reported result-by-result, often as announcements without inspectable artifacts.
• Proof verification depended on peer review, seminars and community reproduction over months to years.
• Full formalization (Lean) was rare for frontier results; it existed chiefly as a research speciality.
• There was no accepted convention for releasing large volumes of machine-produced mathematics.
• AGMAI's recommendations (published 2026-09-29) existed but were untested against a real bulk release.

Change (2026-10-06 onward).

• OpenAI published a bulk public repository (719 manuscripts / 372 families per README; 722 reported by outlets; Apache-2.0) with Lean artifacts for ~42% of top-line results, 10 reasoning summaries, ~4,000 problems attempted, and an average ~3h ChatGPT-Pro-equivalent compute per result.
• The release cited engagement with AGMAI as a source of guidance, while omitting some artefacts AGMAI recommended (prompts, per-result compute).
• On 2026-10-07, three manuscripts were withdrawn for a sign error and 14 revised — the corpus began behaving like a versioned software artifact with errata.
• The mathematics community split publicly: AGMAI (diplomatic, "important event," not an endorsement); AHM (condemnation, boycott call); individual mathematicians ranging from "Mathocalypse" alarm to pragmatic adaptation.

After (state as of 2026-10-13).

• An active, ongoing community effort to digest, re-explain and independently check hundreds of AI-authored mathematical arguments.
• A contested norm: AI labs may release unverified frontier mathematics at scale, with community consent neither sought nor required.
• New infrastructure expectations: formalization status labels, version history, errata and citation practice for machine-authored proofs.
• Unresolved questions about attribution, training-data provenance, and whether solution-without-understanding counts as mathematical progress.

FACT (as described by OpenAI). The vast majority of results were obtained with the same procedure using an unreleased internal OpenAI model. On average, each result used three hours of ChatGPT Pro thinking compute. Across the evaluation the model was posed approximately 4,000 problems. Outputs were aggregated into result families and manuscripts requiring "an appropriate level of significance," producing the catalogue.

FACT. Many proofs have accompanying Lean formalizations (a programming language in which proofs are machine-checked). The repository provides a Lean library, a formalization.yaml catalogue, Comparator challenge instructions, and per-manuscript citation blocks. Roughly 42% of top-line results are formalized (300/719).

FACT (direct repository inspection, 2026-10-13). The lean/ directory is structured as a Lean 4 project pinned to leanprover/lean4:v4.34.1, with a ComparatorChallenges/ set of ~416 .json/.lean pairs, and the formalization.yaml catalogue carries its own machine-readable status block. Crucially, that catalogue self-declares status.scope: "Partial progress.", automation.methods: [agent], and review.status: unchecked. The formalization catalogue's sources: list names 173 papers and its status.main_results: block lists 200 comparator_config declarations over 189 distinct challenge configurations — a different count basis from the README's "300/719" figure. Comparator challenge stubs declare the target theorem and end in sorry, while the mapped solution module implements it (no sorry), with permitted axioms (propext, Quot.sound, Classical.choice) stated per challenge. The ComparatorChallenges/README.md explicitly notes that several configurations verify supporting results, not the corresponding papers' main theorems.

FACT. OpenAI published 10 abridged "reasoning summaries" covering results such as ordinary two-point correlations of multiplicative functions, the irrationality exponent of π, the Mahler conjectures, NP-hardness at the semidefinite threshold, quasipolynomial bounds for arithmetic progressions, Kaplansky's direct-finiteness conjecture, the Mézard–Parisi formula, spontaneous magnetization in the quantum Heisenberg ferromagnet, isomorphism of free group factors, and the relativistic Vlasov–Maxwell system.

INDEPENDENT EVIDENCE. Scott Aaronson (UT Austin) reports that the model "merely" solves roughly 10% of the longstanding open problems it is asked, after a single three-hour attempt, referencing OpenAI's ~4,000-problem figure. He also reports, citing unnamed sources, that cryptography is conspicuously absent from the release and that AI companies are probing weaknesses in cryptographic primitives.

INDEPENDENT EVIDENCE. Dana Moshkovitz (UT Austin), working through the released proof of the Unique Games Conjecture, described the proof as relying on "a completely new bizarre code with a noise test" and "some alien craziness," with citations "often irrelevant and confusing," and said "it's impossible to read it without AI help." Lean formalization was present for that result, but formalization verifies logical correctness of the stated theorem, not exposition, relevance or originality.

INTERPRETATION. The pipeline is therefore: internal model + open problem → long-form proof draft → optional Lean formalization → bulk public release → community digestion/errata. The undisclosed and unverifiable links are the prompting policy, problem selection, and the model itself (which OpenAI has not released).

INTERPRETATION. Formal mathematics is a demanding benchmark for long-horizon reasoning precisely because its outputs are checkable in principle. If a model can produce hundreds of correct, checkable results across subfields in hours, that is strong evidence of capability gains in domains that require extended, self-consistent argument — not just fluent text.

FACT/INDEPENDENT EVIDENCE. Independent mathematicians treat the event as field-defining. Quanta's math editor framed it as mathematics "never being the same"; Scientific American described 372 results whose mere parse "will take mathematicians months"; Retraction Watch documented immediate errata. The disagreement is not about whether something significant happened but about what should count as progress.

INTERPRETATION. The release also became a test case for governance. AGMAI's recommendations (deposit in community-controlled repositories; publish model name, prompts, chain of thought, time and compute per result; formalize where possible; fund human understanding; do not treat releases as marketing) are the first community-authored standard aimed squarely at bulk AI mathematical output. The release followed some and skipped others, and the community's assessment of that gap is now the live question.

INTERPRETATION. For anyone relying on AI outputs in high-assurance domains, the story supplies a concrete, dated caution: a vendor released hundreds of authoritative-looking technical documents, three of which were withdrawn within a day, and stated that some unformalized results "could have issues."

FACT. Public, inspectable access to a large corpus of AI-produced mathematical manuscripts, with a versioned history and partial machine-checkable proofs, for the first time at this scale.

COMPANY CLAIM. OpenAI says the work can "push the frontier of human knowledge and enable further progress in mathematics," that it is funding workshops, conferences and special programmes around understanding major AI-produced results, and that it is "working to responsibly release the model that produced these results."

INTERPRETATION. Looking past the vendor framing, several genuinely new things became possible:

• A community can now study how a model constructs long arguments by reading abridged reasoning traces, giving a partial window into machine mathematical style ("alien" constructions, weak citation practice).
• Formalization-first review become viable at scale: the corpus ships with Lean artifacts for a large minority of results and tooling (Comparator) to check them.
• Errata-as-practice: a public changelog for mathematical claims from a lab, which is unusual and potentially useful for trust calibration.
• A reference case for how (and how not) to release AI-generated scientific output, usable by regulators, journals and other labs.

• How many of the 372 families contain results that are correct, novel and independently understood?
• Does the ~42% formalization coverage hold up under independent Lean checking, including Comparator challenges and kernel assumptions?
• What was the actual problem-selection process, and how were the ~4,000 attempted problems chosen? (AGMAI recommended publishing exactly this.)
• Will vendors publish per-result prompts and compute, as AGMAI recommended, or continue with averages?
• Does the unreleased internal model get released, and on what safety basis?
• How should journals, arXiv and funders treat machine-authored mathematics released outside peer review?
• Does the "single prompt, single agent" claim hold up under independent scrutiny?
• What is the true status of results that were withdrawn and of work that cites them?
• Will the workshops/conferences OpenAI promised materialise and be independently governed, per AGMAI's insistence on nonprofit decision-making?
• Do comprehension failures ("unreadable," "alien") represent a transient exposition problem or a structural limit on human understanding of machine proofs?

FACT / observed trajectory (to 2026-10-13): immediate errata (3 withdrawals, 14 revisions on 2026-10-07); published statements from AGMAI (Oct 6) and AHM (Oct 7); expert commentary and digestion efforts (Quanta, Scientific American, Retraction Watch, Tao, Aaronson, Moshkovitz); a call for boycott; Tao's "Math 2.0" framing and related posts.

PREDICTION (low-to-moderate confidence):

• Further withdrawals/corrections will appear as independent reading proceeds, consistent with independent experts' expectation of "more errors."
• Formalization coverage will increase, but independent Lean re-checking of the whole corpus will take much longer.
• OpenAI will likely release or preview the producing model, given its stated intent, subject to safety review.
• Community/repository norms will harden toward provenance metadata (model, prompts, compute, formalization status), community-hosted mirrors, and clearer labelling of unverified results.
• Individual results (e.g. the Unique Games Conjecture proof, algorithm improvements) will become "results of the year" in their areas once digested, or will be revised/refuted; the corpus is unlikely to remain a single undifferentiated block.
• Governance friction will continue between labs, AGMAI-style advisory bodies and activist groups over consent, attribution and pacing.

FACT-led framing. OpenAI published a public repository of machine-produced mathematics — 719 manuscripts in 372 families per its README (722 per several outlets), ~42% of top-line results formalized, ~4,000 problems attempted, ~3 hours of ChatGPT-Pro-equivalent compute on average — after consulting the independent AGMAI group, which then said publication was "a first step," not an endorsement. Within a day, three manuscripts were withdrawn for a sign error. (Source: OpenAI post and repository; AGMAI; Retraction Watch.)

The honest headline is not "AI solved hundreds of maths problems." It is: a lab released hundreds of machine-authored proofs for the world to verify, and the world has barely started; the release is real and inspectable, the progress claim is the vendor's, and independent verification is the open question. The pairing of released artifacts with expert advice is a genuinely better evaluation pattern than self-reported scores — but only if the verification actually follows. As of 2026-10-13, it has not, and early errata show why the distinction between published, claimed, and verified must be kept explicit.

Why it matters beyond mathematics (INTERPRETATION). This is the clearest case yet of a general pattern: AI producing consequential technical artefacts faster than the institutions that validate knowledge can absorb them. The lesson for any downstream consumer — engineer, enterprise, journalist, citizen — is procedural: demand provenance, check before you build, and treat "artifacts exist" and "results are established" as different categories.

Evidence-label summary