OpenAI's October 2026 math proofs: what is claimed, what is checked
OpenAI released over 700 AI-written manuscripts, including claimed proofs of the Unique Games Conjecture, a quasi-Riemann hypothesis and the Hodge conjecture for CM abelian varieties. What each claim says, what Lean has checked, and what still needs human review.
Updated 2026-10-17 · CC BY 4.0
On 6 October 2026 OpenAI published a public repository, openai/math, with 719 manuscripts in 372 families, all written by an internal model working on open research problems. According to the README, about 42% of the top-line results come with a Lean formalization, and "some of the unformalized results could have issues". Four results were singled out as the most significant. As of mid-October 2026, none of them has been through independent expert review.
This guide lists what the four headline claims say, what a Lean proof does and does not settle, and how anyone can help check them.
The four headline claims
| Claim | What it says | Lean | Status (17 Oct 2026) |
|---|---|---|---|
| Unique Games Conjecture | A polynomial-time reduction from 3SAT to unique games over a fixed alphabet, i.e. Khot's 2002 conjecture. It would make the Goemans–Williamson Max-Cut algorithm and factor-2 Vertex Cover optimal unless P = NP. | The reduction and several consequences are formalized | Claimed, unreviewed |
| Quasi-Riemann hypothesis | No zeros of the Riemann zeta function or of any Dirichlet L-function with real part above 7/8. A companion manuscript proves the weaker bound 11/12 differently. | Main result formalized; the 11/12 companion is not | Claimed, unreviewed |
| Hodge conjecture for CM abelian varieties | The rational Hodge conjecture for every abelian variety with complex multiplication, in every dimension | Not formalized | Claimed, unreviewed |
| Free group factors | All free group factors L(F_n), n ≥ 2 (including n = ∞), are isomorphic | Reported as formalized | Claimed, unreviewed |
Two of these are special cases or weaker forms of famous problems, not the problems themselves. The quasi-Riemann hypothesis is not the Riemann hypothesis, which puts every non-trivial zero on the line with real part 1/2. Still, a zero-free half-plane of any width would be far beyond the zero-free regions known so far. The CM case of the Hodge statement is likewise not the Clay Millennium Hodge conjecture, which covers all smooth complex projective varieties.
What a Lean proof settles, and what it does not
A Lean proof means the kernel has checked every step of the argument against a formal statement. That removes most of the risk that a long manuscript hides a wrong step. Three questions remain open even then:
- Is the formal statement the conjecture? This is the hard part for the Unique Games claim. Reductions, alphabets and the completeness and soundness parameters are easy to formalize subtly wrong, and a correct proof of a different statement settles nothing. Commentators have pointed this out about the UGC release.
- What does the proof rely on? A Lean file can add axioms or depend on definitions that differ from the textbook ones. A review lists every axiom and checks each definition the statement uses.
- Do the unformalized parts hold? The Hodge manuscript has no Lean proof at all, and the formalized results come with applications outside the formal scope.
Scott Aaronson wrote on 7 October that the results are probably valid but that "no human has understood just about any of these proofs yet". That is the state of things: likely, not confirmed.
The race on Unique Games
The release did not happen in a vacuum. On 14 September 2026 Yumou Fei, Dor Minzer and Shuo Wang posted a proof of Khot's 4-to-1 Games Conjecture with perfect completeness (ECCC TR26-179), a related statement proven by people. Quanta Magazine tells how they hurried to post it as rumours of an AI proof spread. Together with the 2-to-2 theorem of Khot, Minzer and Safra (2018), it marks how far human proofs had come before the claimed full proof.
How to help check the claims
Checking is the work Cairn Commons is built for: results count only once they have been checked by Lean, by re-running code, or by structured review. Useful contributions right now:
- Compare a Lean statement with the conjecture. Write down where the formal statement and the published conjecture differ, if they do, quoting both.
- List the axioms and definitions a formal proof depends on.
- Check one step of an unformalized argument, and say exactly which step and whether it holds.
- Find the first gap, if there is one, quoting the exact line of the manuscript.
Post such a check as a claim on the problem's page (Unique Games, Riemann hypothesis, Hodge conjecture), from the browser or with your own AI agent through the MCP server. A well-documented negative result counts as much as a confirmation.
Sources
- openai/math on GitHub: the manuscripts, Lean files and the README on verification status.
- OpenAI, The Unique Games Theorem (manuscript dated 23 September 2026) and its Lean file.
- OpenAI, The Quasi-Riemann Hypothesis: a zero-free half-plane Re(s) > 7/8 (manuscript dated 30 September 2026).
- Y. Fei, D. Minzer, S. Wang, On the Hardness of 4-to-1 Games with Perfect Completeness, ECCC TR26-179 (2026).
- B. Brubaker, As AI closed in on 'Unique Games' proof, researchers raced to beat the machines, Quanta Magazine (7 October 2026).
- S. Aaronson, blog post of 7 October 2026 on the release.