# OpenAI Ships Two Lean-Checked Proofs While David Gross's Group Holds the Yang-Mills Third

> OpenAI's Oct. 26 release pairs a subexponential 3-SAT algorithm and a local smoothing proof with Lean files, David Gross's group holds the Yang-Mills proof, and Anthropic posts a matching 3-SAT result.

- Published: 2026-10-26
- Author: Ryan Elliott Dennis
- Company: OpenAI
- Canonical: https://si-infra.com/journal/openai-lean-checked-proofs-yang-mills-held
- Ledger move: +0.4 Capability (reported). Reading after Oct. 26, 2026: 4.6% of the way to superintelligence on the public record.

OpenAI published three results from an internal model on Oct. 26, 2026: a deterministic algorithm that counts the satisfying assignments of 3-SAT formulas in subexponential time, a proof of Christopher Sogge's 1991 local smoothing conjecture, and an existence proof for four-dimensional Yang-Mills theory [1]. Lean, a program that checks formal proofs line by line, covers the first two. The third sits with a physics group led by Nobel laureate David Gross, and the public has seen only the claim [8].

## What did OpenAI release on Oct. 26, and how much of it has a proof checker behind it?

OpenAI's release history lists four entries for Oct. 26. Local smoothing for the Euclidean wave equation carries a Lean formalization. The Exponential Time Hypothesis result is under examination by an outside group, and the Hodge conjecture entry for CM abelian varieties carries a Lean file as well [1]. A fourth entry, a computation on mutually unbiased bases in dimension six, rests on a Python checker.

The collection behind them is large. OpenAI's README counts 721 manuscripts in 373 families, drawn from about 4,000 posed problems at an average of three hours of ChatGPT Pro thinking compute per result [2]. The README also tells readers how to take them: "In our view, these manuscripts are best understood as a form of raw research data, rather than polished academic papers." That sentence hands the checking to the readers.

How much checking exists? The Oct. 7 entry of the history page puts formalized top-line results at 300 of 719, about 42 percent, which leaves 419 results unchecked by Lean by this desk's arithmetic [1]. That entry withdraws three papers because a sign error invalidates a key argument, and it lists 14 repaired manuscripts. A model that writes at this volume also makes mistakes at this volume, and OpenAI's own page shows it.

## Why does Anthropic's matching 3-SAT result count as outside evidence?

Anthropic posted its own preprint on Oct. 27, titled "A 2^{o(n)} Time Algorithm for 3-SAT," and it reaches the same conclusion by a separate route [4]. The provenance statement reads: "The core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input." A second sentence names the rival: "Independently and concurrently, an internal model at OpenAI claims to have proven a similar result."

Two dates line up. AI Weekly reports that OpenAI's model produced its disproof on Oct. 16 and that Lean formalized it the next day [9]. Two labs, two models, one date and one conclusion: that is replication of a kind the ledger can weigh, because OpenAI's own account could have been wrong in ways that Anthropic's run would have missed.

Read Anthropic's verbs. Its own model "found" the algorithm, while OpenAI's model "claims to have proven" a similar one. The preprint grants the rival a claim and keeps the finding for itself. It also tags its text "Primarily AI-generated" and leaves open which parts of the result Lean covers [4]. Scientific American reports that Anthropic's counter-result came hours after OpenAI's announcement [5].

## What does Lean certify about the ETH claim?

Lean certifies a statement, and OpenAI's scope note says which one. For a fixed clause width k of at least 2, Lean proves that a deterministic machine counts exactly the satisfying assignments of an encoded k-CNF formula on n variables in time of the form (L+1)^O(1) times 2^O(n (log log n)^2 / sqrt(log n)), using polynomial space [3]. The sharper bound in terms of clause count appears in the October 25 manuscript, and the Lean file leaves it out.

The exponent n times (log log n)^2 over the square root of log n grows more slowly than n, so the running time is subexponential. WinBuzzer stresses that this is an asymptotic scaling claim, with a measured speedup on ordinary software still absent, and that Lean confirms a formal argument proves a stated theorem while leaving open whether the formal definitions capture the intended problem [6]. Both points bound the claim. A theorem about a machine encoding can differ in small ways from the hypothesis that hundreds of papers assume.

Three complexity theorists now check that gap. Russell Impagliazzo and Ramamohan Paturi of UC San Diego and Ryan Williams of MIT run the examination, and OpenAI made its materials public at their request [1]. Their open letter says: "Our involvement should not be taken as certification of the claim." [8] The verb they chose is "certification," the word a press release would borrow, and they decline it in advance. Impagliazzo, Paturi and Williams signed up to read the proof, and the letter keeps that job apart from endorsing it.

## Why does the Yang-Mills proof stay private while its Lean file is finished?

The Advisory Group on Mathematics and Artificial Intelligence, a panel of nine mathematicians that includes Timothy Gowers and Edward Witten, posted a statement on Oct. 26. "We call on OpenAI to make public without delay the natural-language and Lean outputs behind its announced existence proofs," it reads [7]. It continues: "By their own account this is now complete, so there is no scientific reason for delaying the release any further." AGMAI also lists the arrangement it objects to: OpenAI said it delayed release until the Lean formalization was complete, and it now reports completion.

David Gross's group holds the material, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov. It plans to write its own explanation before releasing the model's material [8]. The claim covers existence of four-dimensional gauge theories including QCD, and it leaves the mass gap open, so the Clay Mathematics Institute's $1 million prize stays unclaimed.

Can anyone outside that group judge it? Roland Bauerschmidt of New York University, speaking about the late-1980s Balaban papers on which this program builds, told Scientific American: "But I think there's no one who understands these papers and can tell whether they're correct or not." [5] His sentence puts the difficulty in the foundation: a proof that extends Balaban's program rests on papers that few people can read.

A public attempt shows the cost. Levent Alpöge of Anthropic and Ethan Sussman of Northwestern used Claude to generate thousands of pages toward the same program and wrote a repository around them. Its disclaimer says: "we believe it is essentially correct and have done our best to reach a reasonable state of confidence." [10] The repository also states that "Its content has not been satisfactorily vetted." Two groups of careful people, then, describe their own AI-generated physics as tentative.

## Why does the step stop at 0.4?

The capability component asks whether public systems clear the definition's thresholds on tests that stay uncontaminated. A formal proof of a long-standing conjecture is the cleanest test the field has, since Lean checks the logic and the mathematics community checks the statement. Two labs reaching the same ETH result from separate models on Oct. 16 is the kind of confirmation that earns a step. The method's band for reported evidence runs from 0.3 to 0.8, and the ledger places this move at 0.4.

Four facts hold it near the floor. Impagliazzo, Paturi and Williams have yet to report an outcome. Lean covers a narrower statement than the headline, and the sharper clause-count bound lives in a manuscript. OpenAI's Oct. 7 withdrawals show that unchecked papers contain sign errors. The third result, the one closest to a Millennium Prize problem, is out of public reach, and only 42 percent of the catalogue has a Lean file.

What would each side need to be true? Anthropic's side needs the reviewers to find the Lean statement faithful to ETH, so the replication stands. Bauerschmidt's side needs the Yang-Mills material to stay hidden or to contain gaps in Balaban's foundations. The verdict is to credit the convergence on 3-SAT, hold the step at 0.4, and move the reading further only when the reviewers publish or AGMAI receives the Yang-Mills files.

## By the numbers

- 300 of 719 top-line results had Lean formalizations on OpenAI's Oct. 7 ledger entry, about 42 percent [1].
- Three papers were withdrawn on Oct. 7 after a sign error invalidated a key argument, and 14 more were repaired [1].
- OpenAI's catalogue holds 721 manuscripts in 373 families, from about 4,000 posed problems [2].
- About three hours of ChatGPT Pro thinking compute per result is the average OpenAI reports [2].
- Fourteen million output tokens produced Anthropic's 3-SAT algorithm on Oct. 16, with "no human input," per Anthropic [4].
- Three theorists, Impagliazzo, Paturi and Williams, examine the ETH claim, and all three decline to certify it [8].
- Five physicists in Gross's group hold the Yang-Mills material, and the mass gap stays open [8].

## What to watch

The first signal is the Impagliazzo, Paturi and Williams verdict on whether Lean's statement matches the Exponential Time Hypothesis. A published check that the sharper clause-count bound holds would extend the result past what Lean covers [3]. AGMAI's request for the Yang-Mills Lean and natural-language files is the second signal, and Gross's written explanation is the third [7]. A flaw found in the Lean statement, a second withdrawal list, or Anthropic's paper naming what its Lean file covers would each move the reading.

## Sources

1. OpenAI, "OpenAI math: release history," OpenAI (GitHub), October 26, 2026, https://github.com/openai/math/blob/main/history.md
2. OpenAI, "OpenAI math: README," OpenAI (GitHub), October 26, 2026, https://github.com/openai/math
3. OpenAI, "OpenAI math: Lean scope note for the Exponential Time Hypothesis result," OpenAI (GitHub), October 26, 2026, https://github.com/openai/math/blob/main/lean/docs/378.md
4. Anthropic, "A 2^{o(n)} Time Algorithm for 3-SAT," Hexagon, October 27, 2026, https://hexagonmath.org/2610.00577v1
5. Scientific American staff, "Dueling proofs from OpenAI and Anthropic astound scientists," Scientific American, October 27, 2026, https://scientificamerican.com/article/dueling-proofs-from-openai-and-anthropic-astound-scientists
6. WinBuzzer staff, "OpenAI Claims AI-Generated Algorithm Can Solve Some Hard Computing Problems Faster, Overturning The Exponential Time Hypothesis," WinBuzzer, October 27, 2026, https://winbuzzer.com/2026/10/27/openai-claims-ai-generated-algorithm-solves-certain-hard-computing-problems-faster-in-theory-xcxwbn
7. AGMAI, "Recommendation for Immediate Release of Yang-Mills AI Output," Advisory Group on Mathematics and Artificial Intelligence, October 26, 2026, https://agmai.org
8. Interesting Engineering staff, "OpenAI claims major proofs in math, computing and quantum physics," Interesting Engineering, October 26, 2026, https://interestingengineering.com/ai-robotics/openai-proofs-math-computing-physics
9. AI Weekly staff, "OpenAI Hands ETH, Kakeya, Yang-Mills Proofs to Reviewers," AI Weekly, October 26, 2026, https://aiweekly.co/alerts/openai-hands-eth-kakeya-yang-mills-proofs-to-reviewers
10. Ethan Sussman and Levent Alpöge, "Yang-Mills LLM experiment," GitHub, October 27, 2026, https://github.com/ethanwsussman/Yang--Mills-LLM-experiment

## Images

- ![David Gross, a gray-haired physicist, speaking on stage at the Global Young Scientists Summit](https://si-infra.com/img/openai-lean-checked-proofs-yang-mills-held/1.jpg) Nobel laureate David Gross at the Global Young Scientists Summit in Singapore in January 2016; his group now holds OpenAI's Yang-Mills material, announced Oct. 26, 2026. (Photo: Sinednov, Wikimedia Commons, CC BY-SA 4.0, https://commons.wikimedia.org/wiki/File:David_Gross_at_GYSS_19Jan2016_1.jpg)
- ![Tilted stainless-steel facade of the Stata Center at MIT beside a yellow tower and a brick wing](https://si-infra.com/img/openai-lean-checked-proofs-yang-mills-held/2.jpg) The Ray and Maria Stata Center at MIT, home institution of Ryan Williams, one of three theorists examining OpenAI's Exponential Time Hypothesis claim. (Photo: Rhododendrites, Wikimedia Commons, CC BY-SA 4.0, https://commons.wikimedia.org/wiki/File:Stata_Center_(05689p)2.jpg)
- ![A speaker on a stage in front of a projected slide at the GOSIM Paris 2026 conference](https://si-infra.com/img/openai-lean-checked-proofs-yang-mills-held/3.jpg) Timothy Gowers at the GOSIM conference in Paris on May 5, 2026; he sits on the AGMAI panel that asked OpenAI to release the Yang-Mills files on Oct. 26. (Photo: Bretwa, Wikimedia Commons, CC0, https://commons.wikimedia.org/wiki/File:Timothy_Gowers_at_GOSIM_conference_at_Station_F_in_Paris_-_2026-05-05.jpg)

## Sources

1. OpenAI math: release history (OpenAI (GitHub), 2026-10-26) https://github.com/openai/math/blob/main/history.md
2. OpenAI math: README (OpenAI (GitHub), 2026-10-26) https://github.com/openai/math
3. OpenAI math: Lean scope note for the Exponential Time Hypothesis result (OpenAI (GitHub), 2026-10-26) https://github.com/openai/math/blob/main/lean/docs/378.md
4. A 2^{o(n)} Time Algorithm for 3-SAT (Hexagon, 2026-10-27) https://hexagonmath.org/2610.00577v1
5. Dueling proofs from OpenAI and Anthropic astound scientists (Scientific American, 2026-10-27) https://scientificamerican.com/article/dueling-proofs-from-openai-and-anthropic-astound-scientists
6. OpenAI Claims AI-Generated Algorithm Can Solve Some Hard Computing Problems Faster, Overturning The Exponential Time Hypothesis (WinBuzzer, 2026-10-27) https://winbuzzer.com/2026/10/27/openai-claims-ai-generated-algorithm-solves-certain-hard-computing-problems-faster-in-theory-xcxwbn
7. Recommendation for Immediate Release of Yang-Mills AI Output (Advisory Group on Mathematics and Artificial Intelligence, 2026-10-26) https://agmai.org
8. OpenAI claims major proofs in math, computing and quantum physics (Interesting Engineering, 2026-10-26) https://interestingengineering.com/ai-robotics/openai-proofs-math-computing-physics
9. OpenAI Hands ETH, Kakeya, Yang-Mills Proofs to Reviewers (AI Weekly, 2026-10-26) https://aiweekly.co/alerts/openai-hands-eth-kakeya-yang-mills-proofs-to-reviewers
10. Yang-Mills LLM experiment (GitHub, 2026-10-27) https://github.com/ethanwsussman/Yang--Mills-LLM-experiment

Method: https://si-infra.com/method · Ledger: https://si-infra.com/ledger · Founding paper: https://si-infra.com/whitepaper