By verification grade
2 of 14 carry an independent check. Open the review queue.
Open longest before falling
- 177 yrPrime gaps at most 186, conditional on three unproved Lean axiomsposed 1849 · GPT-6 Astra
- 96 yrLean disproof of Krempa's matrix form of the Koethe conjectureposed 1930 · GPT-6 Astra (pre-release)
- 80 yrDisproof of the Erdős unit-distance conjectureposed 1946 · GPT-5 series reasoning model
- 64 yrErdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statementposed 1962 · GPT-6 Astra (pre-release)
From the 9 of 14 entries recording a posed year. Add a missing one.
| Date | Finding | Lab | Model | Verification | Autonomy | Field |
|---|---|---|---|---|---|---|
| 2026-09-08 | Finite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and D | OpenAI | Unnamed OpenAI model described as more capable than GPT-6 Astra for the proof; GPT-6 Astra through Codex for the Lean formalization | Claimed | AI-led | mathematics |
| 2026-09-08 | Finite-time blowup for the unforced Euler equations from smooth compactly supported data | OpenAI | Unnamed OpenAI model described as more capable than GPT-6 Astra for the proof; GPT-6 Astra through Codex for the Lean formalization | Claimed | AI-led | mathematics |
| 2026-09-05 | Disproof of the Ibragimov-Iosifescu conjecture for phi-mixing sequences | OpenAI / Epoch AI | GPT-6 Astra (pre-release) | Claimed | AI-led | mathematics |
| 2026-09-03 | Lean disproof of Krempa's matrix form of the Koethe conjecture | OpenAI / Epoch AI | GPT-6 Astra (pre-release) | Formally verified | Autonomous | mathematics |
| 2026-09-03 | Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement | OpenAI / Epoch AI | GPT-6 Astra (pre-release) | Formally verified | Autonomous | mathematics |
| 2026-09-03 | Counterexample to Smale's mean value conjecture at K = 1 | OpenAI / Epoch AI | GPT-6 Astra (pre-release) | Claimed | Autonomous | mathematics |
| 2026-09-02 | Prime gaps at most 186, conditional on three unproved Lean axioms | OpenAI | GPT-6 Astra | Claimed | AI-led | mathematics |
| 2026-08-01 | Ten results in mathematics and theoretical computer science with Lean certificates | OpenAI | Astra | Formally verified | AI-led | mathematics |
| 2026-07-10 | Cycle double cover conjecture proved for all bridgeless multigraphs | OpenAI | GPT-5.6 Sol Ultra | Formally verified | AI-led | mathematics |
| 2026-05-20 | Disproof of the Erdős unit-distance conjecture | OpenAI | GPT-5 series reasoning model | Independently checked | AI-led | mathematics |
| 2026-01-13 | Erdős problem #728 resolved and formalized in Lean | OpenAI / Harmonic | GPT-5.2 Pro + Aristotle | Formally verified | Autonomous | mathematics |
| 2025-11-20 | Early science acceleration experiments with GPT-5 | OpenAI | GPT-5 | Peer reviewed | AI-assisted | computer-science |
| 2025-10-19 | GPT-5 "solved 10 Erdős problems": it located existing solutions | OpenAI | GPT-5 | Already known | Retrieval | mathematics |
| 2025-08-01 | Improved step-size bound in smooth convex optimization | OpenAI | GPT-5 Pro | Already known | AI-assisted | mathematics |