Notes from Việt Nam on law, technology, languages, history, culture and travel.

719 Manuscripts, 42% Machine-Checked: Inside OpenAI's Unique Games Math Dump

On the evening of 6 October 2026, OpenAI pushed a public GitHub repository called openai/math. It holds research mathematics produced by an unreleased internal model. The README lists 719 manuscripts grouped into 372 “families”. A family is a principal result plus companion papers, consequences or alternative proofs. The headline item is a manuscript titled The Unique Games Theorem. If it is correct, it settles the most influential open conjecture in approximation complexity since Subhash Khot posed it in 2002.

Last week this blog covered Meta’s six Muse Spark papers. Each was co-written by named mathematicians who digested the output before publishing. OpenAI did the opposite: it released hundreds of undigested proofs at once and left the community to sort them out. Scott Aaronson summed up the mood when he wrote that no human appears to have understood just about any of the proofs yet.

What was released, according to the primary source

The repository README is unusually specific about method, so it is worth quoting closely:

  • Model: “an unreleased internal OpenAI model”. OpenAI says it expanded open-problem evaluations “after performance on our existing mathematical evaluations saturated.”
  • Compute: “On average, each result used three hours of ChatGPT Pro thinking compute with that model.”
  • Volume: “the model was posed approximately 4,000 problems”. The outputs were then aggregated into families, with a significance bar applied.
  • Exceptions: work on a zero-free region for the Riemann zeta function and the Hodge Conjecture for CM abelian varieties did not follow the fixed procedure. The Re(s) > 11/12 write-up was human-edited for readability.
  • Reasoning traces: abridged reasoning summaries for 10 families. These include the irrationality exponent of π, Kaplansky’s direct-finiteness conjecture in characteristic two, and NP-hardness at the basic semidefinite threshold, which is the Unique Games family.

An OpenAI spokesperson told Scientific American that the model “produced almost every one of the results in response to a single prompt handed to a single AI agent,” though some may have taken several attempts. That contrasts sharply with OpenAI’s September Navier–Stokes result, which used a swarm of roughly 10,000 agents.

What “Lean-verified” actually means here

This is the part developers should read carefully. Lean is a proof assistant. If a theorem compiles against mathlib, the kernel has checked every logical step. OpenAI ships a large Lean library and a set of Comparator challenge files. Comparator, from the leanprover GitHub organisation, checks a submitted proof against a fixed, human-readable statement of the theorem. Anyone can run, for example, lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json from the lean/ directory.

Three caveats matter:

  1. Coverage is partial. After the 7 October update, the repository’s history file reports “300 / 719 = ~42%” of top-line results formalized. Press figures range from 162 to 300 depending on when and what was counted. The README says plainly that unformalized results “could have issues.”
  2. A formal proof certifies the formal statement, not the paper. The Unique Games scope note is a good example. What was formalized is a deterministic polynomial-time reduction from 3SAT to bipartite unique games over an alphabet 𝔽₂ˢ, with completeness ≥ 1−ε and soundness ≤ δ for every fixed 0 < ε, δ < ½. That is the NP-hardness form of the conjecture. Whether the Lean statement faithfully captures what complexity theorists mean is still a human judgement. The catalogue’s own review: status field reads “unchecked”.
  3. Errors are already surfacing in the informal papers. On 7 October OpenAI withdrew three Hodge-related manuscripts after a sign error broke a stabilization-trace cancellation argument. It also revised 14 others with “proof repairs, corrected statements, clearer hypotheses.” None of the withdrawn papers had a formal proof of its main result. That is exactly the failure mode Lean exists to catch.

The Unique Games result, in context

The Unique Games Conjecture says that, for unique-constraint games, telling almost-satisfiable instances apart from almost-unsatisfiable ones is hard. Its importance comes from its corollaries. It would make the Goemans–Williamson algorithm optimal for Max-Cut and factor 2 optimal for Vertex Cover. OpenAI’s family includes separate formalized manuscripts for both, plus Min-UnCut and directed feedback vertex set.

Quanta Magazine reported that a human team was racing the machines. Dor Minzer and his students Yumou Fei and Shuo Wang heard rumours of an OpenAI proof in September. Three days later they posted a 95-page paper proving the weaker 4-to-1 variant, capping about seven years of work. Dana Moshkovitz has spent years on the conjecture. She said the OpenAI paper was so poorly written that reading it without AI help was “impossible”. She later told Aaronson she had largely followed it with AI assistance. Princeton’s Mark Braverman offered the sharpest line: “Math by press release is not that healthy for math.”

Why this matters beyond mathematics

For the IT industry, the important number is not 372. It is three hours of Pro-tier compute per result. Research-grade proof search now looks like an inference workload: you can schedule it, parallelise it and budget for it. The verification side, meanwhile, looks like software engineering. There is a monorepo, a build that can fail if Linux’s vm.max_map_count is too low, a specification per theorem, and a CI-style checker. This is the same split that coding agents are pushing on software teams. Generation is getting cheap, so the bottleneck moves to specification and review. The Hodge withdrawals show what happens when a claim ships without a machine-checked spec.

There is also a security angle. Aaronson notes that cryptography is conspicuously absent from the list and that labs are quietly probing whether models can break cryptographic primitives. OpenAI has reported no such result. Still, a model that claims results such as L = BPL and new circuit lower bounds on a few hours of compute each is relevant to anyone planning post-quantum migration timelines.

Open questions

  • Reproducibility. An advisory group of mathematicians assembled by OpenAI on 21 September recommended publishing the model, the exact prompts and the per-result compute. OpenAI released only averages and 10 reasoning summaries. It says it takes the guidelines seriously but “is not bound by” them. MIT’s Andrew Sutherland: “We should ask for receipts.” Until the model ships, the single-prompt claim cannot be tested.
  • Selection. The README does not give a failure count or define the significance bar. So “~4,000 problems posed” cannot be turned into a clean success rate.
  • Credit and community. The Association for Human Mathematics has urged mathematicians to stop working with OpenAI. Terence Tao called the pace of lab-generated results “insane”. Daniel Litt, by contrast, expects the release to be good for mathematics. Unlike Meta’s or Anthropic’s curated write-ups, this release leaves the digestion work to unpaid outsiders.

The fairest reading is that machine-checked fragments of this release are already significant, and the rest is a very large, very fast preprint server with a single author. The next few months of human refereeing will show which parts hold.

Sources