How AI impacts theoretical computer science
AI is affecting the field in two ways. Labs and researchers now credit AI models with results on problems that stood open for years or decades, and people in the field are arguing over what that means for credit, training and careers. This page tracks the results. Of the 12 below, 7 have a Lean formalization listed by their repository (4 that the repository lists as covering the main statement, the rest in part), 1 has a public check of the Lean statement against the paper, at least in part, and 0 have a peer-reviewed publication we could find, as of . This site reports who said what. It does not judge whether any proof is correct.
Asking about programming jobs or a general CS degree? This page covers complexity theory and algorithms, so start with the Bureau of Labor Statistics outlook instead. For theory careers, see is theoretical computer science dead?
The ledger
- Public record found
- Partial record
- None found as of 2026-11-01
A filled box means a public record exists. It does not mean the proof is right. You can download this table as JSON.
Result by result
Open a result to read the claim as written, each source and every named statement we found.
ETH: refutation claims
- Before
- ETH, from Impagliazzo and Paturi, conjectured s_k > 0 for k ≥ 3. Best earlier 3-SAT records cited by Anthropic: O(1.328^n) deterministic, O(1.308^n) randomized. Source (2026-10-26)
- Claim, as written
- OpenAI abstract: (n + m)^{O_k(1)} 2^{n/(log n)^{1/2+o(1)}}. OpenAI Theorem 1.1: (n + m)^{O_k(1)} 2^{O_k(n log log n/√log n)}; m ⩽ Dn: (n + m)^{O_{k,D}(1)} 2^{O_{k,D}(n/√log n)}. Anthropic Theorem 1: 2^{O(min{k^2 n log log n/√log n, km/√log m})}. Anthropic Theorem 2: O(2^{δn}) for every δ > 0. Anthropic Corollary 5: s_k = 0 for every k ≥ 3; s_∞ = 0. Source (2026-10-25)
- Claimed by
OpenAI, 2026-10-26: The Exponential Time Hypothesis is False. Source
Anthropic, 2026-10-27: A 2^{o(n)} Time Algorithm for 3-SAT. Source
- AI role, per source
- OpenAI README attributes manuscripts to an unnamed internal model; ETH-specific procedure unstated. Anthropic's paper states internal Claude found core algorithm October 16, 14M output tokens, no human input. Source (2026-10-26)
- Lean, per repository
- OpenAI lean/ComparatorChallenges/SubexponentialSAT.lean: weaker (log log n)^2 exponent, not Theorem 1.1. Anthropic eth/MainResults.lean: Main Theorem and ETH negation on Mathlib multi-stack machines. Source (2026-10-26)
- Lean statement checked
- Toledo (Claude-written tools; first statement reading by Claude Opus 5.5) bridged each statement to Lean ETH per lab's model; model step stays prose. Busnello hand-read both, one encoding check unfinished. Source (2026-10-28)
- Named experts
Russell Impagliazzo, Ramamohan Paturi, Ryan Williams, 2026-10-26: Their open letter says participation is not certification and asks the community for independent scrutiny, explanations and follow-up study of the claim. Source
Ryan Williams, 2026-10-26: Says the three organizers signed no NDAs, receive no pay, and will share findings publicly; says OpenAI agreed to release materials and sponsor a conference. Source
Ryan Williams (to TechCrunch), 2026-10-27: Called some proof parts perhaps routine and two or three alien-looking; does not think OpenAI's algorithm can be the best achievable. Source
Ryan Williams, 2026-10-27: Conditional on correctness, every computer scientist should raise their P=NP credence somewhat, by varying amounts. Source
Lance Fortnow, 2026-10-28: States he has not checked the proof himself yet considers it safe to assume ETH is finished; notes Lean covers a slightly weaker bound. Source
Scott Aaronson, 2026-10-26: Reported the claim as roughly exp(n/√log(n)) for 3SAT, and moved his personal P=NP probability from 3% to 5%. Source
Emanuele Viola, 2026-10-27: Wrote that the manuscript shows ETH and strong ETH false, said he is not shocked, and hopes conditional results get recalibrated. Source
Ben Recht, 2026-10-28: Calls OpenAI's algorithm galactic, running an exponential-time subroutine when variables number below 10^10,000,000,000,000,000,000,000,000. Source
Ryan O'Donnell, 2026-10-30: LLM-assisted exposition recasting OpenAI's approach through sparse permanents; deterministic sparse case, with a randomized appendix for arbitrary 3-CNFs. Source
Shiva Kintali, 2026-10-26: Posted a simplified exposition of OpenAI's proof, developed with Claude and ChatGPT then expanded by hand, aiming only at basic ETH. Source
Mark Sellke (Member of Technical Staff at OpenAI, per his homepage), 2026-10-29: Slides outline OpenAI's 2^{o(n)} k-SAT algorithm, credit the theorem to OpenAI/Anthropic 2026, and skip quantitative optimizations. Source
Francis Zane, 2026-10-30: Reports people compiling the Lean proofs locally; opens a replication thread, suggesting a non-author should probably check though not everyone needs to repeat it. Source
- Peer review
- No peer-reviewed publication found as of 2026-11-01. Searched both repositories, Hexagon, ethdiscussion.blog, OpenAlex and web search.
- Revisions
- OpenAI paper dated 17 October, revised 25 October; one repository commit touches the PDF. Anthropic's Hexagon page lists version 1 only. No retraction found as of 2026-11-01. Source (2026-11-01)
- Last checked
3SUM: truly subquadratic time
- Before
- Textbook O(n^2) improved only by polylogarithmic factors; 3SUM hypothesis postulated n^{2-o(1)} for polynomial-size integers on word RAM with O(log n)-bit words. Source (2026-10-05)
- Claim, as written
- Abstract and Theorem 2: O(n^{1.9992}). Theorem 22: n^{2−1/1296+o(1)} ≤ O(n^{1.99923}) using Theorem 5; n^{2−ε′/2+o(1)} ≤ O(n^{1.9992}) using Corollary 26. Theorem 2, real inputs: O(n^{1.998}) expected time, Las Vegas. Lean: ThreeSum.SolvedInTime 1.9992. Source (2026-10-05)
- Claimed by
Alman, Vassilevska Williams, 2026-10-05: Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs. Source
Anthropic (Lean), 2026-10-06: Truly Subquadratic 3SUM and Truly Subcubic APSP: a Lean 4 formalization. Source
- AI role, per source
- Paper states Claude discovered the hypothesis-refuting algorithm, average then worst case, in a 16M-output-token session without human input; authors understood, simplified, strengthened, extended, and take responsibility. Source (2026-10-05)
- Lean, per repository
- anthropics/formal-math 3sum-apsp/EndStatement.lean: Theorem_22_3SUM, plus Theorems 19, 22 and Corollary 39 zero-weight. README excludes real-input Theorem 35, reductions' printed running times, and Theorem 33. Source (2026-10-06)
- Lean statement checked
- No named public check of 3sum-apsp Lean statements against the paper found. Searched ethdiscussion.blog, Toledo's reports, Busnello, repository docs, GitHub, arXiv and web search (as of 2026-11-01).
- Named experts
Scott Aaronson, 2026-10-07: Said the preprint refutes half-century-old conjectures, credited an Anthropic model with the crucial idea, and contrasted digested release with OpenAI's raw one. Source
Virginia Vassilevska Williams (co-author), 2026-10-13: Co-author says the proof came from an internal Anthropic model, not the authors; argues, from one run each, her group's 2023 notes plus two prompts would have sufficed. Source
Emanuele Viola, 2026-10-06: Reacted with surprise and added the paper to his book's growing list of disproved conjectures. Source
Sankeerth Rao Karingula (Agentin AI), Shachar Lovett (UC San Diego), 2026-10-11: Give a simplified proof of polynomial 3SUM and APSP improvements with weaker exponents, using selected-entry matrix multiplication; disclose an Agentin AI agent swarm, ChatGPT and Codex. Source
Ruhollah Majdoddin, 2026-10-12: Extends the matrix theorem to D <= N^0.172 and claims deterministic 3SUM in n^{1.9945+o(1)}, citing the original exponent as 1.9992. Source
Nick Fischer, 2026-10-23: Treats the 3SUM Hypothesis as recently refuted, says geometric lower bounds lost their foundation, and recovers many under the k-AP Hypothesis. Source
- Peer review
- No peer-reviewed publication found as of 2026-11-01. Searched arXiv metadata, OpenAlex, Crossref, web search. Co-author Vassilevska Williams wrote she is reluctant to submit to STOC. Source
- Revisions
- arXiv lists only v1, dated 2026-10-05; no revision or withdrawal recorded as of 2026-11-01. Source (2026-11-01)
- Last checked
APSP: truly subcubic time
- Before
- Classical O(n^3); fastest prior algorithm shaved only a subpolynomial 2^{Ω(√log n)} factor. APSP hypothesis postulated n^{3−o(1)} for polynomially bounded integer weights on word RAM. Source (2026-10-05)
- Claim, as written
- Abstract and Theorem 2: O(n^{2.9995}). Theorem 22: Õ(n^{3−1/1944}) ≤ O(n^{2.99949}) using Theorem 5; Õ(n^{3−ε′/3}) ≤ O(n^{2.99942}) using Corollary 26, with ε′ = 0.00175. Theorem 2, real inputs: O(n^{2.998}) expected time, Las Vegas. Lean: APSP.SolvedInTime 2.99942. Source (2026-10-05)
- Claimed by
Alman, Vassilevska Williams, 2026-10-05: Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs. Source
Anthropic (Lean), 2026-10-06: Truly Subquadratic 3SUM and Truly Subcubic APSP: a Lean 4 formalization. Source
- AI role, per source
- Paper states Claude discovered the hypothesis-refuting algorithm, average then worst case, in a 16M-output-token session without human input; authors understood, simplified, strengthened, extended, and take responsibility. Source (2026-10-05)
- Lean, per repository
- 3sum-apsp/EndStatement.lean: Theorem_22_APSP and Theorem_22_MinPlus at 2.99942; README lists wordRam_theorem_22_first for 2.99949 route. README: no machine proof for real-weight Theorem 35, Theorem 33 or directed-unweighted Theorem 34 running times. Source (2026-10-06)
- Lean statement checked
- No named public check of 3sum-apsp Lean statements against the paper found. Searched ethdiscussion.blog, Toledo's reports, Busnello, repository docs, GitHub, arXiv and web search (as of 2026-11-01).
- Named experts
Scott Aaronson, 2026-10-07: Reported APSP at O(n^2.9995), said this refutes a half-century-old conjecture, and credited an Anthropic model with the crucial idea. Source
Virginia Vassilevska Williams (co-author), 2026-10-13: Co-author says the proof came from an internal Anthropic model, not the authors; argues, from one run each, her group's 2023 notes plus two prompts would have sufficed. Source
Sankeerth Rao Karingula (Agentin AI), Shachar Lovett (UC San Diego), 2026-10-11: Give a simplified proof of polynomial 3SUM and APSP improvements with weaker exponents, using selected-entry matrix multiplication; disclose an Agentin AI agent swarm, ChatGPT and Codex. Source
Ruhollah Majdoddin, 2026-10-12: Claims n^{2.9945+o(1)} for Exact Triangle, (min,+)-product and APSP, citing the original APSP exponent as 2.99942. Source
Barna Saha, Christopher Ye, 2026-10-14: Claim deterministic (min,+) product in Õ(N^{2.9964}), improving the O(N^{2.9995}) they attribute to Anthropic via Alman and Vassilevska Williams, using its thin matrix theorem. Source
- Peer review
- No peer-reviewed publication found as of 2026-11-01. Searched arXiv metadata, OpenAlex, Crossref, web search. Co-author Vassilevska Williams wrote she is reluctant to submit to STOC. Source
- Revisions
- arXiv lists only v1, dated 2026-10-05; no revision or withdrawal recorded as of 2026-11-01. Source (2026-11-01)
- Last checked
Unique Games Conjecture
- Before
- Khot stated it in a 2002 paper. Khot–Minzer–Safra's 2018 report (ECCC TR18-006) says it completes the 2-to-2 conjecture, with imperfect completeness. Quanta describes Unique Games as open before OpenAI's announcement. Source (2026-10-07)
- Claim, as written
- [Paper, Theorem 1.1] For every fixed ε, δ ∈ (0, 1/2), there are an integer s ≥ 1 and a deterministic polynomial-time reduction from 3SAT to explicit unweighted Unique Games instances G_φ over K = F_2^s such that φ satisfiable ⟹ val(G_φ) ≥ 1 − ε, φ unsatisfiable ⟹ val(G_φ) ≤ δ. [Paper, abstract] We prove the Unique Games Conjecture. [CONTENTS.md, family 102] Proves Khot's Unique Games Conjecture. [lean/ComparatorChallenges/UniqueGamesTheorem.lean] theorem theorem11 (ε δ : ℝ) (hε : 0 < ε) (hεhalf : ε < 1 / 2) (hδ : 0 < δ) (hδhalf : δ < 1 / 2) : Nonempty (Explicit.MachineOutputContract.BinaryGapReduction ε δ) Source (2026-09-23)
- Claimed by
OpenAI, 2026-10-06: The Unique Games Theorem. Source
- AI role, per source
- README attributes manuscripts to an unnamed internal OpenAI model, about three hours of ChatGPT Pro compute per result on average; its family 102 reasoning summary concerns basic-semidefinite-threshold NP-hardness. Source (2026-10-30)
- Lean, per repository
- Repo lists the main theorem as formalized: lean/ComparatorChallenges/UniqueGamesTheorem.lean; declaration OAI.UniqueGamesTheorem.theorem11 in lean/OAI/Computability/UniqueGames/Theorem.lean. Scope document: lean/docs/102.md. Source (2026-10-06)
- Lean statement checked
- No named person found confirming the Lean statement equals the paper. Ariel Elboim ran Comparator but says he did not audit this; formalization.yaml's repo-wide review field says unchecked (as of 2026-11-01). Source (2026-10-09)
- Named experts
Scott Aaronson (UT Austin), 2026-10-07: Says he and others are fairly sure it is a proof, citing a Lean certificate, but apparently almost no human has understood these proofs yet. Source
Dana Moshkovitz (UT Austin), texts relayed by Scott Aaronson, 2026-10-07: Her early texts, relayed by Aaronson, call the writeup unreadable without AI help and describe a strange new recursive code, unlike long or short codes. Source
Dana Moshkovitz, relayed by Scott Aaronson (comment #2), 2026-10-07: Aaronson relays her view that the conjecture is true, its famous corollaries did not need it, and understanding the proof's mechanism will take time. Source
Dana Moshkovitz (UT Austin; talk abstract), 2026-10-30: Her talk abstract offers a mental map of the proof, viewing its innovation as a new code, Hadamard with a noise test; says the writeup reads poorly for humans. Source
Scott Aaronson (post and comment #9), 2026-10-31: Says Moshkovitz, his wife, studied the proof closely with Khot, Håstad and Minzer and gave two Simons talks; says they can understand the new code once shown it. Source
Lance Fortnow (former founding dean of computing, Illinois Tech), 2026-10-07: Presents the release as proofs not yet fully verified, and makes his assessment of its significance conditional on whether they hold up. Source
Rares-Darius Buhai, Suprovat Ghoshal, Neng Huang, Pravesh Kothari, Euiwoong Lee, Konstantin Makarychev, Yury Makarychev, 2026-10-19: Their Max-Cut paper uses it conditionally: if OpenAI's proof is correct, one of their hardness results would need only NP not in BPP. Source
Mark Braverman (Princeton), quoted by Quanta, 2026-10-07: Speaking in September about the rumors, he criticized announcing mathematics through press releases, yet said an AI proof could open directions if its key assumptions are extracted. Source
Dor Minzer (MIT), quoted by Quanta, 2026-10-07: Told Quanta that AI tools remove the value of failing and may deter long projects; the article reports no verdict from him on the proof's correctness. Source
Bill Gasarch (University of Maryland), 2026-10-18: On the whole release: warns a Lean check can certify a mis-encoded theorem, and expects humans to read, understand and, where needed, repair these proofs over time. Source
- Peer review
- None found as of 2026-11-01. Manuscript README cites only an OpenAI release preprint; arXiv API and web searches showed no venue; proceedings not checked individually. Source (2026-10-30)
- Revisions
- No revision or withdrawal recorded: paper.pdf and the Lean directory show only the 2026-10-06 initial commit at 4eaee87, and history.md does not list it (as of 2026-11-01). Source (2026-10-30)
- Last checked
2-to-1 games, perfect completeness
- Before
- Fei–Minzer–Wang (ECCC, 2026-09-14) report perfect-completeness hardness for 4-to-1 games, not 2-to-1, crediting Dinur et al. with the almost-perfect version. Austrin et al. (2013 manuscript): 2-to-1 soundness 23/24+ε at perfect completeness. Source (2026-09-14)
- Claim, as written
- [Paper, Theorem 1.1] For every fixed rational δ ∈ (0, 1) there are an integer q = q(δ) ≥ 2 and a deterministic polynomial-time reduction from 3-SAT to 2-to-1 games with alphabets [2q] and [q] such that: (i) a satisfiable formula produces a game of value 1; (ii) an unsatisfiable formula produces a game of value at most δ. [Paper, abstract] We prove the 2-to-1 Games Conjecture with perfect completeness. For every fixed rational δ ∈ (0, 1), it is NP-hard to distinguish satisfiable 2-to-1 games from games of value at most δ, with a fixed alphabet and an explicitly listed unweighted multiset of constraints. [CONTENTS.md, family 105] Proves Khot's 2-to-1 Games Conjecture with perfect completeness [lean/ComparatorChallenges/PerfectCompleteness.lean] theorem exists_reduction (δ : ℚ) (positive : 0 < δ) (less_than_one : δ < 1) : Nonempty (PerfectCompleteness.BinaryGapReduction δ) Source (2026-09-23)
- Claimed by
OpenAI, 2026-10-06: Perfect completeness for 2-to-1 games. Source
- AI role, per source
- Quanta calls it an AI-generated manuscript with no human editing or independent expert review. README attributes manuscripts to an unnamed internal model; no reasoning summary is listed for family 105. Source (2026-10-07)
- Lean, per repository
- Repo lists the main reduction as formalized: lean/ComparatorChallenges/PerfectCompleteness.lean; OAI.PerfectCompleteness.Theorem11.exists_reduction in lean/OAI/Computability/PerfectCompleteness/Theorem11.lean; rational δ in (0,1), exact-two projection tables. Source (2026-10-06)
- Lean statement checked
- No named person found checking the Lean statement against the paper. Fortnow's Claude-prepared note says it did not run the check; formalization.yaml's repo-wide review field says unchecked (as of 2026-11-01). Source (2026-10-30)
- Named experts
- No public statement found as of 2026-11-01
- Peer review
- None found as of 2026-11-01. Manuscript README cites only an OpenAI release preprint; arXiv API and web searches showed no venue; proceedings not checked individually. Source (2026-10-30)
- Revisions
- No revision or withdrawal recorded: paper.pdf and the Lean directory show only the 2026-10-06 initial commit at 4eaee87, and history.md does not list it (as of 2026-11-01). Source (2026-10-30)
- Last checked
L = RL = BPL
- Before
- Hoza (2021) noted deterministic simulation of randomized space S in space O(S^{3/2} / √{log S}), slightly improving Saks–Zhou's O(S^{3/2}). Aaronson (2026) calls L = BPL a great derandomization conjecture. Source (2021-09-15)
- Claim, as written
- [Paper, Theorem 1.1, Exact logarithmic-space derandomization] L = RL = BPL. [Paper, abstract] We prove L = RL = BPL, resolving the derandomization problem for polynomial-time randomized logarithmic space. [CONTENTS.md, family 103] Proves L=RL=BPL, resolving derandomization for bounded-error logarithmic-space computation. [lean/ComparatorChallenges/LogspaceEquality.lean] theorem exact_logarithmic_space_derandomization : L = RL ∧ RL = BPL Source (2026-09-23)
- Claimed by
OpenAI, 2026-10-06: Exact Derandomization of Logarithmic Space: L = RL = BPL. Source
- AI role, per source
- README attributes manuscripts to an unnamed internal OpenAI model, about three hours of ChatGPT Pro compute per result on average; no reasoning summary is listed for family 103. Source (2026-10-30)
- Lean, per repository
- Added 2026-10-08 UTC, commit 3014888: lean/ComparatorChallenges/LogspaceEquality.lean; OAI.ExactDerandomization.exact_logarithmic_space_derandomization in lean/OAI/Computability/Logspace/Equality.lean. Class equality only; compiler bounds not stated. Source (2026-10-08)
- Lean statement checked
- No named person found matching the Lean model to the paper or textbook. Fortnow's Claude-prepared note leaves this open; formalization.yaml's repo-wide review field says unchecked (as of 2026-11-01). Source (2026-10-07)
- Named experts
Scott Aaronson (UT Austin), 2026-10-07: Lists L = BPL among results he will watch, calling it a major derandomization conjecture whose truth was not seriously doubted; says humans have barely begun digesting these proofs. Source
Omer Reingold, relayed by Scott Aaronson, 2026-10-07: In a remark Aaronson shared with permission, he jokes that the RL versus L result was when things turned serious for him; a reaction, not an assessment. Source
Lance Fortnow (former founding dean of computing, Illinois Tech), 2026-10-07: Lists a full derandomization of randomized log space, without the Lean tag given to two neighbours, and says these proofs have not been fully verified. Source
Lance Fortnow (former founding dean of computing, Illinois Tech), 2026-10-15: Wrote that complexity results are hard to formalize, then updated to say OpenAI had released what he terms a claimed Lean proof of L = RL = BPL. Source
Kuan Cheng, Shengtang Huang, Ruiyang Wu, 2026-10-19: Their paper says OpenAI announced BPL = L and argues their L-AC^1 result still offers multiplicative error 2^{-poly log n}; it does not assess OpenAI's proof. Source
- Peer review
- None found as of 2026-11-01. Manuscript README cites only an OpenAI release preprint; arXiv API and web searches showed no venue; proceedings not checked individually. Source (2026-10-30)
- Revisions
- Manuscript unchanged since 2026-10-06. Lean added 2026-10-08 (commit 3014888); comparator JSON definition list emptied 2026-10-26 (commit 42907c9). No withdrawal recorded. Source (2026-10-26)
- Last checked
Matrix multiplication: ω ≤ 9/4
- Before
- Best prior bound found: ω < 2.371177 (Dupont et al., arXiv preprint, 2026-08-17), which it reports as improving the earlier bound of 2.371339. Source (2026-08-17)
- Claim, as written
- [9/4 paper, Theorem 1.1] For every ε > 0, two n × n complex matrices can be multiplied using O_ε(n^{9/4+ε}) arithmetic operations. In particular, ω ≤ 9/4. [9/4 paper, abstract] We prove that the exponent of matrix multiplication over the complex numbers is at most 9/4. [CONTENTS.md, family 107] Proves ω≤9/4 over ℂ, giving O_ε(n^{9/4+ε}) arithmetic operations for square matrix multiplication. [lean/ComparatorChallenges/MatrixMultiplication.lean] theorem complex_omega_le_nine_quarters : Arithmetic.omega ℂ ≤ (9 : ℝ) / 4 [Staggered paper, Theorem 1.1] Over every fixed field F, the arithmetic exponent of square matrix multiplication satisfies ω_F < 2.371054886006746 < 2.371054887. [Complex Matrix Multiplication Below 2.258, abstract] Over every field of characteristic zero, we prove that the square matrix-multiplication exponent satisfies ω < 2.258, the dual exponent satisfies α > 0.465, and ω(1, 0.709, 1) < 2.092. Source (2026-10-02)
- Claimed by
OpenAI, 2026-10-06: An Upper Bound of 9/4 for the Matrix Multiplication Exponent. Source
- AI role, per source
- README attributes manuscripts to an unnamed internal OpenAI model; Shpilka also describes the result as obtained by an OpenAI internal model. No reasoning summary is listed for family 107. Source (2026-10-30)
- Lean, per repository
- Over ℂ only: lean/ComparatorChallenges/MatrixMultiplication.lean, OAI.MatrixMultiplication.complex_omega_le_nine_quarters in lean/OAI/LinearAlgebra/MatrixMultiplication/Main.lean. Every-field target is only ω < 2.371054886006746 (MatrixFields.lean). Source (2026-10-06)
- Lean statement checked
- No named human found certifying the match. Navot's fork reports AI reviews matched the textbook definition exactly for infinite fields; Zuiddam's repo leaves the model question to readers of Model.lean (as of 2026-11-01). Source (2026-10-08)
- Named experts
Steven Strogatz (Cornell), 2026-10-06: Singled out the 2.25 exponent as especially striking, put the earlier record near 2.37, and likened the leap to Bob Beamon's long jump. Source
Scott Aaronson (UT Austin), 2026-10-07: Highlights an n^{9/4+o(1)}-time matrix multiplication result, noting a rational exponent and a completely different approach from earlier bounds. Source
Lance Fortnow (former founding dean of computing, Illinois Tech), 2026-10-07: Lists n^{2.25+ε} time, tagged as formalized in Lean, while cautioning that the release's proofs have not been fully verified. Source
Bill Gasarch (University of Maryland), 2026-10-25: Restates ω(C) ≤ 2.25 and the every-field bound as Lean-formalized, compares the drop to Beamon's jump, and says he has not checked the third-party every-field project. Source
Rafael Pass, 2026-10-20: Says OpenAI claimed the bound via non-constructive spectral arguments; gives an explicit integer-arithmetic algorithm reaching it, with the main ideas his own and Codex used extensively. Source
Alimzhan Amanov, Maxim van den Berg, Jeroen Zuiddam (University of Amsterdam), 2026-10-21: Expound OpenAI's proof, give a version valid for every field, and prove a barrier: current degeneration ingredients cannot improve these bounds. They disclose LLM use. Source
Amir Shpilka (Tel Aviv University), 2026-10-27: States OpenAI's manuscript proves ω ≤ 9/4, gives a self-contained explicit version following its ideas, and says he verified all arguments in his exposition, disclosing AI assistance. Source
Sela Navot, 2026-10-07: Repository reports an extension of the bound to arbitrary fields, found with GPT-6 Astra and GPT-6.1 Sol. Source
Houxi Lü, 2026-10-12: Preprint addresses matrix multiplication in arbitrary characteristic. Source
- Peer review
- None found as of 2026-11-01. The 9/4 manuscript README cites only an OpenAI release preprint; arXiv API and web searches showed no venue; proceedings not checked individually. Source (2026-10-30)
- Revisions
- No revision or withdrawal recorded: the 9/4, 2.258 and every-field manuscripts show only the 2026-10-06 initial commit at 4eaee87; history.md lists none (as of 2026-11-01). Source (2026-10-30)
- Last checked
Subset Sum in O(2^0.49n)
- Before
- Chen, Jin, Randolph and Servedio give worst-case O(2^{n/2} · n^{-γ}) for a constant γ > 0.5023, a polynomial saving over Horowitz–Sahni O(2^{n/2}); their abstract frames time 2^{(1/2 - c)n} as a major goal. Source (2023-01-17)
- Claim, as written
- Title and abstract: O(2^{0.49n}). Theorem 1.1: at most C_c 2^{0.49n} word operations for n ≥ N_c and b ≤ n^c, correct with probability at least 2/3. Intermediate bound: 2^{0.489995n} poly(n + b + 2). Source (2026-10-04)
- Claimed by
OpenAI, 2026-10-06: Subset Sum in Time $O(2^{0.49n})$. Source
- AI role, per source
- Repository-wide, not result-specific: an unnamed internal OpenAI model produced the manuscripts; most results followed one procedure, averaging three hours of ChatGPT Pro thinking compute. It calls them raw research data. Source (2026-10-26)
- Lean, per repository
- No Lean for the 2^{0.49n} result found: family 138 has no listed Lean. Unlisted lean/OAI/Combinatorics/LowSpaceSubsetSum/Main.lean states theorems only for the companion low-space 2^{n/2}-time result (as of 2026-11-01). Source (2026-10-06)
- Lean statement checked
- No named person found comparing Lean statements with these manuscripts. The main 2^{0.49n} result has no Lean statement to compare (as of 2026-11-01).
- Named experts
Lance Fortnow, 2026-10-07: Batch-level remark: Fortnow wrote the release's proofs had not been fully verified and framed his assessment as conditional on them holding up; he does not name this result. Source
Lance Fortnow, 2026-10-28: Fortnow wrote the ETH-refuting algorithm adds nothing for Subset Sum, whose best algorithms he described as still taking roughly 2^{n/2}; the post body does not mention the 0.49 manuscript. Source
Lance Fortnow (blog comment), 2026-10-29: Replying to a commenter who pointed to OpenAI's 2^{0.49n} claim, Fortnow called it impressive but not 2^{o(n)}; he does not say he checked it. Source
Lixi Ye and Baitian Li, 2026-10-07: Ye and Li note OpenAI released a similar-type result and report their own O(2^{0.499999n}) algorithm, developed independently by another route; they do not assess OpenAI's proof. Source
Ce Jin and Xiao Mao, 2026-10-14: They cite both OpenAI Subset Sum manuscripts among references on exponential-time and average-case work, offering no assessment of their correctness. Source
- Peer review
- No peer-reviewed publication found as of 2026-11-01
- Revisions
- No revision or withdrawal recorded: only the initial commit touches this folder, the PDF blob matches at adc7f12 and 4eaee87, and history.md does not name it (as of 2026-11-01). Source (2026-10-29)
- Last checked
Deterministic polynomial factoring
- Before
- Altman (2025) calls deterministic polynomial-time factoring over finite fields a notorious open problem and says no method for arbitrary polynomials over F_p is known even under GRH. Source (2025-09-16)
- Claim, as written
- Theorem 1.1: prime p in binary, nonzero dense f ∈ F_p[x] of degree n, complete factorization in O(((n + 1)⌈log_2 p⌉)^{10^{12}}) bit operations. Imported from companion, Theorem 11.1: no zero in ℜs > 1 − δ, δ = 10^{−6}. Source (2026-10-04)
- Claimed by
OpenAI, 2026-10-06: Deterministic Polynomial Factorization over Prime Fields. Source
- AI role, per source
- Repository-wide, not result-specific: an unnamed internal OpenAI model produced the manuscripts; most results followed one procedure, averaging three hours of ChatGPT Pro thinking compute. It calls them raw research data. Source (2026-10-26)
- Lean, per repository
- No formalization listed: no lean/docs/142.md or 029.md, no CONTENTS Lean link, neither manuscript in lean/formalization.yaml, and no matching Lean file name found (as of 2026-11-01). Source (2026-10-26)
- Lean statement checked
- No Lean statement exists to compare, and no named public check was found (as of 2026-11-01).
- Named experts
Pierre-Jean Spaenlehauer, 2026-10-23: Spaenlehauer treats the factoring result as OpenAI's claim, resting on a companion zero-free preprint; he writes the community had not reviewed or validated it and no formalized proof existed. Source
Scott Aaronson, 2026-10-07: Aaronson listed GRH-free deterministic factoring among results he expected to watch most; he reported no check and said it appeared humans had understood almost none of these proofs yet. Source
Lance Fortnow, 2026-10-07: Batch-level remark: Fortnow wrote the release's proofs had not been fully verified and framed his assessment as conditional on them holding up; he does not name this result. Source
Jizhou Guo, 2026-10-08: Guo's AI-compiled note derives deterministic irreducible-polynomial construction conditional on family 142 Theorem 1.1 and family 029 Theorem 1.2, adding that neither family lists a Lean formalization; it verifies neither. Source
- Peer review
- No peer-reviewed publication found as of 2026-11-01
- Revisions
- No revision or withdrawal recorded: only the initial commit touches this folder or the companion's, the PDF blob matches at adc7f12 and 4eaee87, and history.md does not name it (as of 2026-11-01). Source (2026-10-29)
- Last checked
PCP for PPAD: quasilinear reduction
- Before
- Conjecture 2 of Babichenko, Papadimitriou and Rubinstein asked that End of the Line reduce quasilinearly to (ε, δ)-Gcircuit; they note the δ = 0 time-hardness form already followed from Conjecture 1. Source (2015-04-09)
- Claim, as written
- Abstract: output circuit's total binary length is N(log N)^{O(1)}. Theorem 1.3 (Quasilinear PCP for PPAD): fixed rational constants 0 < ε < 1/10, 0 < δ < 1; M ≤ AN⌈log_2(N + 2)⌉^b. Source (2026-09-25)
- Claimed by
OpenAI, 2026-10-06: The PCP-for-PPAD conjecture: a quasilinear reduction. Source
- AI role, per source
- Repository-wide, not result-specific: an unnamed internal OpenAI model produced the manuscripts; most results followed one procedure, averaging three hours of ChatGPT Pro thinking compute. It calls them raw research data. Source (2026-10-26)
- Lean, per repository
- No Lean proof of the main result found. lean/OAI/Computability/GeneralizedCircuits/Mesh.lean states QuasilinearPCPStatement as an unproved goal and proves only supporting lemmas, per its header; absent from formalization.yaml (as of 2026-11-01). Source (2026-10-06)
- Lean statement checked
- No named person found comparing QuasilinearPCPStatement with the manuscript's Theorem 1.3. That statement is only a goal proposition in the repository (as of 2026-11-01).
- Named experts
Panagiotis Kanellopoulos and Themistoklis Melissourgos, 2026-10-19: A footnote describes the manuscript as generated with an OpenAI model and claiming the quasilinear version; the authors know of no independent verification so far. Source
Ioannis Panageas, Avi Shein, Shayan Taherijam and Vijay V. Vazirani, 2026-10-26: The authors say they have not independently verified OpenAI's claimed proof and keep their constant-error hardness result conditional on PCP for PPAD. Source
Xiaotie Deng, Ningyuan Li, Zihe Wang and Jie Zhang, 2026-10-19: They say the OpenAI preprint reports a proof of the conjecture, giving no assessment; their own conditional hardness rests on Rubinstein's theorem and PPAD-ETH instead. Source
Lance Fortnow, 2026-10-07: Batch-level remark: Fortnow wrote the release's proofs had not been fully verified and framed his assessment as conditional on them holding up; he does not name this result. Source
- Peer review
- No peer-reviewed publication found as of 2026-11-01
- Revisions
- No revision or withdrawal recorded: only the initial commit touches this folder, the PDF blob matches at adc7f12 and 4eaee87, and history.md does not name it (as of 2026-11-01). Source (2026-10-29)
- Last checked
MAX-4-CUT hardness: 0.987
- Before
- Best prior NP-hardness factor cited by the authors: 85/86 + ε (about 0.9883), from Austrin, O'Donnell, Tan, Wright, Theorem 1.2, stated for k-Coloring with k = 4. Source
- Claim, as written
- arXiv v7 Theorem 3.2: (0.9349 − ε, 0.9238 + ε)-approximating MAX-4-CUT, hence NP-hard to 0.987 + ε-approximate. Abstract and Google blog: 0.987, improving 0.9883. Lemma C.2: c = 49535, s_1 = 49538, s_2 = 48681, count = 52941. Source (2026-03-09)
- Claimed by
Nagda, Raghavan, Thakurta, 2025-09-22: Reinforced Generation of Combinatorial Structures: Applications to Complexity Theory. Source
- AI role, per source
- Authors say AlphaEvolve searched for the 19-variable gadget and evolved faster verifiers; they report framing the search, inspecting fast verifiers by hand, and brute-force checking the final gadgets. Source (2026-03-09)
- Lean, per repository
- No Lean or proof-assistant formalization found. arXiv v7 relies on brute-force checking code; its phrase about formal verification refers to standard computation, not a named proof assistant (as of 2026-11-01). Source (2026-03-09)
- Lean statement checked
- No Lean statement found to compare, and no named public check was located (as of 2026-11-01).
- Named experts
- No public statement found as of 2026-11-01
- Peer review
- No peer-reviewed publication found as of 2026-11-01
- Revisions
- Seven arXiv versions, 2025-09-22 to 2026-03-09; 0.987 unchanged in abstracts. v6 retitled. Uri Feige credited for an earlier Appendix B.2 error, which covers average-case upper bounds, not MAX-4-CUT. Source (2026-03-09)
- Last checked
Metric TSP hardness: 111/110
- Before
- Chlebík and Chlebíková improved the TSP hardness value from 123/122 (Karpinski, Lampis, Schmied) to 117/116. Source
- Claim, as written
- arXiv v7 Theorem 4.1: for any ε > 0, NP-hard to approximate metric TSP to within 111/110 − ε. Abstract (v5 to v7): factor 111/110, improving 117/116. Gadget parameters: s(H) = c(H) = 10. Source (2026-03-09)
- Claimed by
Nagda, Raghavan, Thakurta, 2025-11-20: Reinforced Generation of Combinatorial Structures: Applications to Complexity Theory (arXiv v5, first version stating the TSP bound). Source
- AI role, per source
- Authors say AlphaEvolve searched for equation gadgets; this problem needed the most human involvement, with authors modularizing soundness and completeness proofs from earlier work before the search. Source (2026-03-09)
- Lean, per repository
- No Lean or proof-assistant formalization found. The paper reports computational checking of gadgets and a written reduction proof (as of 2026-11-01). Source (2026-03-09)
- Lean statement checked
- No Lean statement found to compare, and no named public check was located (as of 2026-11-01).
- Named experts
- No public statement found as of 2026-11-01
- Peer review
- No peer-reviewed publication found as of 2026-11-01
- Revisions
- Bound first appears in arXiv v5 (2025-11-20), absent from v1 to v4 abstracts; abstract value unchanged through v7 (2026-03-09). No retraction found. Source (2026-03-09)
- Last checked
Why the columns are separate
- A claim is a paper or repository saying a theorem holds.
- A Lean formalization means a proof compiles against a formal statement. The repository decides what is covered, and that is often less than the paper's main theorem.
- A Lean statement check asks a different question: does the formal statement say what the paper and the textbook say? A proof can compile and still answer the wrong question.
- A named expert statement is what a person said in public, including when they said they had not checked.
- Peer review means a journal or conference accepted it. Finding none means only that our search found none.
For the Exponential Time Hypothesis, read how far that claim has been checked. For how this table is built, read the method.
Changelog
- : Ledger published with 12 results. Cells were checked against their linked sources on this date. Sources: the links in each row.