AI × SCIENCE · OPEN PROBLEMS

Unknown, Q.E.D.

Quod erat demonstrandum.

Tracking every scientific problem solved by AI. Each record states how complete the result is, how it was verified and where it came from, and anyone can annotate or challenge it.

Grades

SolvedAI found, or led the way to, a complete and new solution.
PartialAn improved bound, a new construction or a special case; the problem stays open.
Prior artThe “new” solution AI produced was already in the literature.
UnverifiedClaimed publicly but not yet independently checked.

Problems

Newest first · 259 of 262 records
  1. 2026-10-06Math · Analysis
    Littlewood polynomials with large normalized Mahler measureAn internal OpenAI model produced a preprint proving that real ultraflat Littlewood polynomials exist, which settles an Epoch AI open problem; the proof has not yet been independently checked.OpenAI internal model✓ Lean formalization supplied by OpenAI · Marked solved by Epoch AI0 notes
    Unverified
  2. 2026-10-06Math · Mathematics and theoretical CS
    OpenAI's release of 372 result families in mathematicsOpenAI released 719 manuscripts in 372 result families produced by an unreleased model; about 42% are formalized in Lean, none is peer reviewed, and three were withdrawn a day later over a sign error.OpenAI internal model✓ Lean formalizations for about 42% of top-line results0 notes
    Unverified
  3. 2026-09-17Math · Number theory
    Apéry-style irrationality proofs: ζ(5) and Catalan's constantA preprint proving that ζ(5) is irrational, now formalized in Lean by a third party, led Epoch AI to mark this open problem solved by human and AI; no primary source we found describes the AI's role.Aabir Fauzan (ζ(5)); OpenAI internal model (Catalan's constant)✓ Lean formalization of the ζ(5) proof (third party) · Marked solved (human + AI) by Epoch AI0 notes
    Unverified
  4. 2026-09-08Math · Partial differential equations
    Navier–Stokes: OpenAI's claim of finite-time blowup with smooth forcingOpenAI claims an internal model proved that a 3D incompressible fluid starting at rest can develop a singularity in finite time under a smooth external force, one of the four forms of the Millennium Prize problem; the 166-page proof is unverified and its priority is disputed.OpenAI internal model, with GPT-6 Astra for the Lean formalization✓ Lean formalization by OpenAI (its fidelity is disputed)0 notes
    Unverified
  5. 2026-08-20Math · Arithmetic geometry
    Elliptic curves over ℚ of rank at least 30 and 31Claude, working with Levent Alpöge and Ava Howell, found elliptic curves over ℚ with at least 30 and then 31 independent rational points, beating the record of 29 set in 2024.Claude (Anthropic) with Levent Alpöge and Ava Howell✓ Rank ≥ 31 curve verified by ICARM (2026-09-25) · Marked solved (human + AI) by Epoch AI0 notes
    Partial
  6. 2026-08-12Math · Combinatorics
    A Hadamard matrix of order 668Anthropic researcher Levent Alpöge posted Hadamard matrices for every order up to 2000 where none was known, including 668, found by three people working with Claude; an independent check confirmed the matrix, but the method is unpublished.Claude (Anthropic) with three human researchers✓ Matrix checked independently (Nechita, 2026-08-13) · Marked solved by Epoch AI (provisional)0 notes
    Solved
  7. 2026-08-09Math · Number theory
    The inverse Galois problem for the Mathieu group M23Huang, Jackson, Lee, Poonen, Pries and Zhang gave an explicit degree-23 polynomial over ℚ with Galois group M23, the last sporadic simple group not yet realized; Epoch AI credits AI as instrumental, but the paper has not been peer reviewed.Huang, Jackson, Lee, Poonen, Pries and Zhang, with Claude and ChatGPT models✓ Marked solved (human + AI) by Epoch AI0 notes
    Unverified
  8. 2026-08-01Math · Mathematics and theoretical CS
    OpenAI's “ten advances” in mathematics and theoretical computer scienceOpenAI announced ten results produced with GPT-6 Astra, from sphere-packing bounds to Ramsey numbers, with Lean certificates; none has been peer reviewed, and two face credit disputes from mathematicians.GPT-6 Astra (OpenAI)✓ Lean certificates published · Partial independent audit (arXiv:2608.14673)0 notes
    Unverified
  9. 2026-07-30Math · Arithmetic geometry
    A genus-2 curve with a rational torsion point of prime order at least 31GPT-5.6 Sol passed Epoch AI's verifier with such a curve, but the curve came from an existing public database; Epoch itself says the solution was latent in the literature.GPT-5.6 Sol (OpenAI)✓ Passed Epoch AI's verifier0 notes
    Prior art
  10. 2026-07-26Math · Combinatorics
    Shorter superpermutations on 8, 9 and 10 symbolsNew superpermutations shorter than Egan's 2018 bound were posted for 8, 9 and 10 symbols; those for 9 and 10 were developed interactively with GPT-5.6 Sol, which then retrieved them to pass Epoch AI's verifier.William Echols with GPT-5.6 Sol (n = 9, 10); Uku Raudvere (n = 8)✓ Passed Epoch AI's verifier0 notes
    Partial
  11. 2026-06-29Math · Geometry
    Erdős Problem #1070Partial progress by Ákos Dúcz and Dániel Varga with Codex and GPT-5.5 (29 Jun 2026): partial result.Ákos Dúcz and Dániel Varga with Codex and GPT-5.5✓ Listed in Tao's wiki0 notes
    Partial
  12. 2026-06-27Math · Graph theory
    Erdős Problem #1033A claim by GPT-5.5 Pro (27 Jun 2026) that has not yet been verified: candidate partial result.GPT-5.5 Pro✓ Listed in Tao's wiki0 notes
    Unverified
  13. 2026-06-27Math · Number theory
    Erdős Problem #731A claim by Eric Li with GPT (27 Jun 2026) that has not yet been verified: candidate full solution.Eric Li with GPT✓ Listed in Tao's wiki0 notes
    Unverified
  14. 2026-06-24Math · Number theory
    Erdős Problem #1061A claim by Eric Li with GPT (24 Jun 2026) that has not yet been verified: candidate full solution.Eric Li with GPT✓ Listed in Tao's wiki0 notes
    Unverified
  15. 2026-06-24Math · Number theory
    Erdős Problem #730A claim by GPT-5.5 Pro (24 Jun 2026) that has not yet been verified: candidate full solution.GPT-5.5 Pro✓ Listed in Tao's wiki0 notes
    Unverified
  16. 2026-06-23Math · Set theory
    Erdős Problem #1177A claim by Eric Li with GPT (23 Jun 2026) that has not yet been verified: candidate full solution.Eric Li with GPT✓ Listed in Tao's wiki0 notes
    Unverified
  17. 2026-06-23Math · Combinatorics
    Erdős Problem #21Partial progress by Varun Sivashankar with Aristotle and GPT-5.5 Pro (23 Jun 2026): partial result (Lean).Varun Sivashankar with Aristotle and GPT-5.5 Pro✓ Lean formalization · Listed in Tao's wiki0 notes
    Partial
  18. 2026-06-23Math · Number theory
    Erdős Problem #432A claim by Sungchul Lee with GPT-5.5 Pro (23 Jun 2026) that has not yet been verified: candidate partial result.Sungchul Lee with GPT-5.5 Pro✓ Listed in Tao's wiki0 notes
    Unverified
  19. 2026-06-23Math · Set theory
    Erdős Problem #593A claim by Eric Li with GPT (23 Jun 2026) that has not yet been verified: candidate full solution.Eric Li with GPT✓ Listed in Tao's wiki0 notes
    Unverified
  20. 2026-06-22Math · Number theory
    Erdős Problem #1054Partial progress by Claude Opus 4.8, GPT-5.5 Pro and Principia Math (22 Jun 2026): partial result (Lean).Claude Opus 4.8, GPT-5.5 Pro and Principia Math✓ Lean formalization · Listed in Tao's wiki0 notes
    Partial
  21. 2026-06-22Math · Number theory
    Erdős Problem #400A claim by Eric Li with GPT (22 Jun 2026) that has not yet been verified: candidate partial result.Eric Li with GPT✓ Listed in Tao's wiki0 notes
    Unverified
  22. 2026-06-22Math · Number theory
    Erdős Problem #536Partial progress by Codex and GPT-5.5 Pro (22 Jun 2026): partial result (Lean).Codex and GPT-5.5 Pro✓ Lean formalization · Listed in Tao's wiki0 notes
    Partial
  23. 2026-06-22Math · Graph theory
    Erdős Problem #550A claim by GPT (22 Jun 2026) that has not yet been verified: candidate full solution.GPT✓ Listed in Tao's wiki0 notes
    Unverified
  24. 2026-06-22Math · Analysis
    Erdős Problem #671A claim by Codex and GPT-5.5 Pro (22 Jun 2026) that has not yet been verified: candidate full solution (Lean).Codex and GPT-5.5 Pro✓ Lean formalization · Listed in Tao's wiki0 notes
    Unverified
  25. 2026-06-22Math · Number theory
    Erdős Problem #768A claim by Eric Li with GPT (22 Jun 2026) that has not yet been verified: candidate full solution.Eric Li with GPT✓ Listed in Tao's wiki0 notes
    Unverified
  26. 2026-06-21Math · Analysis
    Erdős Problem #1197Full solution by Aristotle, Claude Opus 4.7 and GPT-5.4 Pro, formalized in Lean (21 Jun 2026).Aristotle, Claude Opus 4.7 and GPT-5.4 Pro✓ Lean formalization · Listed in Tao's wiki0 notes
    Solved
  27. 2026-06-21Math · Additive combinatorics
    Erdős Problem #176Partial progress by Codex and GPT-5.5 Pro (21 Jun 2026): partial result (Lean). 2 AI contributions are recorded in all.Codex and GPT-5.5 Pro✓ Lean formalization · Listed in Tao's wiki0 notes
    Partial
  28. 2026-06-21Math · Number theory
    Erdős Problem #346Full solution by Kenta Kitamura with Codex and GPT, formalized in Lean (21 Jun 2026). 2 AI contributions are recorded in all.Kenta Kitamura with Codex and GPT✓ Lean formalization · Listed in Tao's wiki0 notes
    Solved
  29. 2026-06-21Math · Number theory
    Erdős Problem #865Full solution by Ricky Cipollini with GPT-5.5 Pro (21 Jun 2026).Ricky Cipollini with GPT-5.5 Pro✓ Listed in Tao's wiki0 notes
    Solved
  30. 2026-06-21Math · Number theory
    Erdős Problem #948Full solution by Aristotle and GPT-5.5 Pro, formalized in Lean (21 Jun 2026).Aristotle and GPT-5.5 Pro✓ Lean formalization · Listed in Tao's wiki0 notes
    Solved
  31. 2026-06-19Math · Number theory
    Erdős Problem #1139A claim by Przemek Chojecki, gavinsherry, Liam Price and Terence Tao with GPT-5.2 Pro and GPT-5.5 Pro (19 Jun 2026) that has not yet been verified: candidate full solution.Przemek Chojecki, gavinsherry, Liam Price and Terence Tao with GPT-5.2 Pro and GPT-5.5 Pro✓ Listed in Tao's wiki0 notes
    Unverified
  32. 2026-06-19Math · Number theory
    Erdős Problem #451Partial progress by Wouter van Doorn and Quanyu Tang with Aristotle and GPT-5.5 Pro (19 Jun 2026): partial result (Lean).Wouter van Doorn and Quanyu Tang with Aristotle and GPT-5.5 Pro✓ Lean formalization · Listed in Tao's wiki0 notes
    Partial
  33. 2026-06-19Math · Graph theory
    Erdős Problem #81Partial progress by Wouter van Doorn with Aristotle and GPT-5.5 Pro (19 Jun 2026): partial result (Lean).Wouter van Doorn with Aristotle and GPT-5.5 Pro✓ Lean formalization · Listed in Tao's wiki0 notes
    Partial
  34. 2026-06-17Math · Number theory
    Erdős Problem #306Partial progress by Shisheng Li with Claude and Claude Code (17 Jun 2026): partial result (Lean). 2 AI contributions are recorded in all.Shisheng Li with Claude and Claude Code✓ Lean formalization · Listed in Tao's wiki0 notes
    Partial
  35. 2026-06-16Math · Graph theory
    Erdős Problem #986Full solution by Domagoj Bradač with Claude and OpenAI internal model (16 Jun 2026).Domagoj Bradač with Claude and OpenAI internal model✓ Listed in Tao's wiki0 notes
    Solved
  36. 2026-06-14Math · Geometry
    Erdős Problem #1208A claim by Sungchul Lee with GPT-5.5 Pro (14 Jun 2026) that has not yet been verified: candidate partial result.Sungchul Lee with GPT-5.5 Pro✓ Listed in Tao's wiki0 notes
    Unverified
  37. 2026-06-14Math · Number theory
    Erdős Problem #326Full solution by Aron Bhalla with Aristotle, Codex and GPT-5.5, formalized in Lean (14 Jun 2026).Aron Bhalla with Aristotle, Codex and GPT-5.5✓ Lean formalization · Listed in Tao's wiki0 notes
    Solved
  38. 2026-06-10Math · Number theory
    Erdős Problem #539Partial progress by Codex, GPT-5.5 and ProofCouncil (10 Jun 2026): partial result (Lean).Codex, GPT-5.5 and ProofCouncil✓ Lean formalization · Listed in Tao's wiki0 notes
    Partial
  39. 2026-06-09Math · Number theory
    An explicit presentation of the absolute Galois group of ℚ₂AI models produced a candidate explicit presentation of the absolute Galois group of the 2-adic numbers, the one case left open; Lean formalizations exist but rely on cited results, and the write-up is not peer reviewed.Claude Fable 5 (per Epoch AI) and GPT-5.5 Pro, with David Roe and David Turturean✓ Two Lean formalizations relying on cited results · Marked solved by Epoch AI0 notes
    Unverified
  40. 2026-06-09Math · Graph theory
    Erdős Problem #619Full solution by Claude Fable 5, Codex and GPT-5.5, formalized in Lean (9 Jun 2026).Claude Fable 5, Codex and GPT-5.5✓ Lean formalization · Listed in Tao's wiki0 notes
    Solved