Mathematics produced or claimed by AI systems: one short narrated video for every result family in OpenAI's openai/math release. Every tile is a claim, not a refereed theorem: the grades and verdicts are ours, and the article explains what the Lean library does and does not certify.
The number on each tile is our breakthrough score, 0 to 100: how important the problem is, how far the result moves it, what follows if it holds, and how surprising it is. It measures size, not truth; a 100 with no Lean behind it is huge only if it holds. The wall opens biggest first.
- families
- 372
- huge if true
- 13
- manuscripts
- 722
- Lean: main theorem
- 169
- Lean: part
- 67
- videos so far
- 372
All 372 results
100003The quasi-Riemann hypothesis
Number theorylandmarkLean
100197A torsion-free group algebra that is not directly finite
AlgebralandmarkLean · part
100157Graph coloring, clique minors, and Colin de Verdière invariants
CombinatoricslandmarkLean · part
100285Counterexamples to Baum–Connes and Kadison–Kaplansky
Operator algebraslandmarkno Lean
96102The Unique Games Conjecture and optimal approximation thresholds
Theoretical computer sciencelandmarkLean
96159Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi bounds
CombinatoricslandmarkLean · part
94196A counterexample to Kaplansky’s zero-divisor conjecture
AlgebralandmarkLean
94248Thompson's group F is nonamenable
Group theorylandmarkLean
94287Isomorphism of the free group factors
Operator algebraslandmarkLean
94215Canonical O(3) continuum limit and exact O(4) mass asymptotics
Probability and statistical mechanicslandmarkLean · part
94335Gromov’s integral scalar-curvature bound for simplicial volume
Differential geometrylandmarkno Lean
92107Matrix multiplication with exponent at most 9/4
Theoretical computer sciencemajorLean
92103Exact derandomization of logarithmic space: L=RL=BPL
Theoretical computer sciencelandmarkno Lean
87004Hilbert’s tenth problem over ℚ
Number theorylandmarkno Lean
87304The Hilbert–Smith conjecture in every dimension
Topologylandmarkno Lean
86073The Falconer distance conjecture
Real and complex analysislandmarkLean
86161Counterexamples to Sidorenko’s conjecture and the forcing conjecture
CombinatoricslandmarkLean
86252A torsion-free hyperbolic group that is neither residually finite nor linear over any field
Group theorylandmarkLean
86032Hodge and Kuga–Satake results for all projective K3 surfaces
Algebraic and complex geometrylandmarkno Lean
86202The blockwise Alperin weight conjecture
Algebralandmarkno Lean
86305Four-dimensional disk embedding and Wall's conjecture
Topologylandmarkno Lean
86340A counterexample to the nearby Lagrangian conjecture
Differential geometrylandmarkno Lean
82113Approximate counting and entropy of perfect matchings
Theoretical computer sciencelandmarkLean
82246Cannon's conjecture
Group theorylandmarkLean
82254Classifying spaces and geometric obstructions for Artin groups
Group theorylandmarkLean
82288Kadison's similarity conjecture
Operator algebraslandmarkLean
82223Random-cluster interfaces: critical, disordered, thermal, and natural-time scaling
Probability and statistical mechanicslandmarkno Lean
82346Sharp singular-set bounds for stationary integral varifolds
Differential geometrylandmarkno Lean
82120Almost-linear-time exact matching and prescribed-degree factors in general graphs
Theoretical computer sciencemajorno Lean
81017The irrationality exponent of π is 2
Number theorylandmarkLean
79005Irrationality of Catalan’s constant
Number theorylandmarkLean
79087The Mahler conjectures, functional inequalities and polar-product symplectic width
Convex and metric geometrylandmarkLean
79179The circulant Hadamard and Barker-sequence conjectures
CombinatoricslandmarkLean
79198A counterexample to finitistic-dimension finiteness
AlgebralandmarkLean
79199Counterexamples to Auslander–Reiten, Tachikawa and related homological conjectures
AlgebralandmarkLean
79324Lipschitz equivalent Banach spaces need not be linearly isomorphic
Functional analysislandmarkLean