Drawing the map…
Every family, by discipline
Each family is a group of related papers in OpenAI’s catalogue. Open its page to read those papers and the reports about them.
Number theory 31 families, 17 with Lean
- Milne’s rationality conjecture and algebraic specialization
- The full BSD formula from low Selmer corank
- The quasi-Riemann hypothesis
- Hilbert’s tenth problem over ℚ
- Irrationality of Catalan’s constant
- Goldfeld’s conjecture: densities and mean analytic rank
- Ordinary two-point correlations and the corrected Elliott conjecture
- The Deligne–Drinfeld conjecture
- Function-field reconstruction from Milnor K-theory and Galois data
- Unrestricted pro-modularity at the prime two
- Prime-factor statistics of \(p-1\)
- Independent largest prime factors of consecutive integers
- Ostmann’s inverse Goldbach conjecture
- Restricted geometric Langlands, global Arthur enhancements, and generic Ramanujan
- Torus-packet equidistribution in prime, quartic, and sextic degrees
- Zilber–Pink in abelian varieties and the Siegel threefold
- The irrationality exponent of π is 2
- The Margulis–Platonov conjecture over global fields
- The local p-adic section conjecture and global consequences
- Squarefree quartics and power-free polynomial values
- A quadratic bound for Jacobsthal’s function
- The weak inhomogeneous Duffin–Schaeffer conjecture
- Patterson’s first moment for cubic Gauss sums
- An asymptotic formula for the number of totients
- Short Egyptian fractions
- Positive lower density of large prime gaps
- Potential integral density on curve character varieties
- Uniformly bounded components of Gaussian-prime graphs
- Primitive roots for every admissible integer base
- Modularity of elliptic curves over imaginary quadratic fields
- Uchida’s conjecture for open homomorphisms of Galois groups
Algebraic and complex geometry 36 families, 8 with Lean
- The rational Hodge conjecture for CM abelian varieties
- Iitaka subadditivity, variation, and logarithmic additivity
- Log abundance for compact Kähler spaces under logarithmic Iitaka subadditivity
- Log-canonical threefold abundance in numerical dimension one
- Numerical semiampleness and generalized minimal models
- The ordinary-double-point volume gap
- Fujita’s freeness conjecture
- Nagata’s conjecture and maximal Seshadri constants
- Bloch’s conjecture for complex surfaces
- Hyperkähler SYZ and projective-space bases
- Oka classification for minimal compact complex surfaces: Kodaira dimension zero and class VII
- P = W for fixed-determinant SLn moduli spaces
- The equivariant cohomological Hikita conjecture
- Shafarevich counterexamples in dimension two and with large fundamental group
- Zariski cancellation and affine fibrations over the complex numbers
- A characteristic-zero counterexample to Lipman–Zariski
- A stable-coordinate counterexample in four variables
- A counterexample to Griffiths’ positivity conjecture
- Kobayashi’s canonical-ampleness conjecture
- Tangent splittings and product decompositions
- A counterexample to Pixton completeness in Chow
- Irrational cubic fourfolds with Hodge-theoretic and categorical K3 associations
- Gepner symmetry and large-volume stability on threefolds
- Termination of projective and Kähler fourfold minimal model programs
- Fundamental groups of special complex varieties and root orbifolds
- Semialgebraic universal covers and bounded domains
- Counterexamples to Zariski’s multiplicity conjecture
- The Global Spherical Shell conjecture
- Projective contact classification and the LeBrun–Salamon conjecture
- The generalized Mukai conjecture
- Topological triviality of μ-constant surface singularities
- Virasoro constraints for complete intersections and projective-bundle towers
- Bounded klt complements for Fano contractions
- The Campana–Peternell conjecture in dimension six
- Anticanonical nonvanishing in every dimension
- Global quantum geometric Langlands at irrational level
Real and complex analysis 16 families, 10 with Lean
- Koebe’s circle-domain conjecture
- Brennan’s conjecture and the integral-means spectrum
- The Falconer distance conjecture
- Kakeya in three and four dimensions
- The \(L\log L\) Fourier-convergence conjecture
- Real ultraflat Littlewood polynomials and unbounded binary merit factors
- Fourier restriction for positively curved surfaces
- The three-dimensional Bochner–Riesz conjecture
- Local smoothing in three dimensions
- The exact Sobolev endpoint for Schrödinger convergence
- Riesz transforms and rectifiability in higher codimension
- Annular variation and dyadic absolute bounds for the triangular Hilbert transform
- Hilbert transforms along Lipschitz directions
- The geometric case of the Erdős similarity conjecture
- Endpoint Sobolev regularity of centered disk averages
- An L3 bound for the trilinear Hilbert transform
Convex and metric geometry 15 families, 13 with Lean
- The Mahler conjectures, functional inequalities and polar-product symplectic width
- Sharp projection-body inequalities and a counterexample to simplex maximization
- Bounded-distortion L1 embeddings of planar and bounded-treewidth graphs
- Triangular-lattice optimality, long-range Riesz and Coulomb energies, and spherical logarithmic energy
- Logarithmic and Lp Brunn–Minkowski inequalities and the B-conjecture
- The optimal order of convex-body covering density
- Dimension-free logarithmic Sobolev inequality for subgaussian log-concave measures
- Subpolynomial dimension reduction in Lp
- Hyperbolicity cones without semidefinite lifts
- The Gaussian propeller conjecture in every dimension
- The Euclidean Steinitz–Bergström bound
- Compact counterexamples to bi-Lipschitz dimension reduction
- The sharp exponential scale of edit-distance distortion
- Cylinder coverings below the half-area bound
- The sharp simplex conjecture for isotropic constants
Theoretical computer science 40 families, 34 with Lean
- The Unique Games Conjecture and optimal approximation thresholds
- Exact derandomization of logarithmic space: \(\mathsf L=\mathsf{RL}=\mathsf{BPL}\)
- Quasipolynomial algorithms for mean-payoff, stochastic and parity games
- Perfect completeness for 2-to-1 games
- Hardness of coloring three-colorable graphs
- Matrix multiplication with exponent at most 9/4
- A cubic permanent–determinant lower bound
- Integer multiplication below \(n\log n\)
- Optimal-order randomized k-server on arbitrary metrics
- One-sample matroid prophet inequalities against an almighty adversary
- Beyond the square-root exponent for depth-three circuits
- Approximate counting and entropy of perfect matchings
- Approximate counting of common integer polymatroid bases
- Sampling and counting contingency tables with arbitrary margins
- Uniform black-box noncommutative identity testing across characteristics
- Uniform sparsest cut: hardness and semidefinite gaps
- Bin packing and unbounded configuration-LP gaps
- The Courtade–Kumar and Hellinger conjectures
- Almost-linear-time exact matching and prescribed-degree factors in general graphs
- Almost-linear approximation of edit distance
- Quantitative trace-reconstruction bounds with a uniform decoder
- Polynomial-time scheduling on three identical machines
- The metric k-median approximation threshold and recovery
- Exponential semidefinite complexity of perfect matching
- Average sensitivity of polynomial threshold functions
- A factor-two approximation for shortest common superstring
- Exponential state costs for two-way automata
- Exact Fourier transforms below \(n\log n\)
- Rapid mixing of graph switches for every degree sequence
- A superquadratic separation of sensitivity and block sensitivity
- The computational complexity of Weisfeiler–Leman refinement
- Generalized star height at most three
- Homogeneous depth-five lower bounds for iterated matrix multiplication
- A quasilinear PCP theorem for PPAD
- One-tape time simulation in two-fifths-power space
- Subset Sum in \(O(2^{0.49n})\) time
- Subpolynomial query complexity for log-concave sampling
- Memory–sample lower bounds for noiseless Gaussian regression
- Existential–universal real sentences in the counting hierarchy
- Deterministic polynomial factorization over prime fields
Dynamical systems and ergodic theory 12 families, 9 with Lean
- Hilbert’s sixteenth problem: uniform bounds for limit cycles
- Banach’s simple Lebesgue-spectrum problem
- Rokhlin’s multiple-mixing problem
- Positive metric entropy for the standard map
- The near-boundary Birkhoff conjecture
- The entropy-rate dimension formula for self-similar measures
- Classwise permanence for weakly reversible mass-action systems
- Weak mixing of triangular billiards with an irrational angle
- A C1 counterexample to the entropy conjecture
- Zero entropy does not guarantee a smooth positive-volume model
- Arithmetic classification and non-Pisot singularity for Bernoulli convolutions
- Pointwise multiple ergodic averages for mixing transformations
Combinatorics 37 families, 33 with Lean
- A counterexample to periodic tiling in dimension three
- Borsuk’s conjecture fails in dimension nine
- Graph coloring, clique minors, and Colin de Verdière invariants
- The Euclidean plane cannot be colored with five colors
- Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi bounds
- Superexponential van der Waerden numbers
- Counterexamples to Sidorenko’s conjecture and the forcing conjecture
- Counterexamples to Ryser’s covering conjecture
- Hindman’s finite sums and products conjecture
- The Harary–Hill and Zarankiewicz crossing-number formulas
- The higher-dimensional Erdős distinct-distances conjecture
- Planar distinct distances and unit-distance bounds
- Combinatorial invariance of Kazhdan–Lusztig polynomials
- Shareshian–Wachs elementary positivity
- Sharp logarithmic exponents for off-diagonal Ramsey numbers
- The hypercube Ramsey conjecture
- Classification of finite Euclidean Ramsey configurations
- Seymour’s second-neighborhood conjecture
- Deterministic construction of strong thin spanning trees
- Talagrand’s expectation thresholds, discrete convexity, and graph decompositions
- The second Kahn–Kalai conjecture with an edge-count bound
- Bounded-degree coboundary expanders
- Deterministic nonbipartite Ramanujan graphs in every fixed degree
- The circulant Hadamard and Barker-sequence conjectures
- Barnette’s Hamiltonian-cycle conjecture
- The Erdős–Gallai cycle-decomposition conjecture
- Power savings for intersective polynomial differences and prime arguments
- Power savings for planar halving lines and k-sets
- Correspondence coloring with a fixed forbidden subgraph
- Counterexamples to infinite matroid intersection and packing/covering
- Uniform influence and sharp thresholds for graph and hypergraph properties
- Snaky in 21 Maker moves
- The sharp terminal leave in random triangle removal
- Cycle–clique Ramsey numbers
- Polynomial removal fails for ordered binary matrices
- A power improvement in the Heilbronn triangle lower bound
- Boolean functions violate the square-root degree bound by arbitrary factors
Algebra 18 families, 10 with Lean
- Serre’s intersection-multiplicity conjecture
- Lech’s multiplicity conjecture
- A counterexample to the small Cohen–Macaulay module conjecture
- A counterexample to Kaplansky’s zero-divisor conjecture
- A torsion-free group algebra that is not directly finite
- A counterexample to finitistic-dimension finiteness
- Counterexamples to Auslander–Reiten, Tachikawa and related homological conjectures
- Eisenbud–Green–Harris and lex-plus-powers
- A counterexample to Kurosh’s division-ring problem
- The blockwise Alperin weight conjecture
- Donovan’s conjecture over fields and complete mixed-characteristic DVRs
- Tensor saturation for even spin groups
- Saxl’s conjecture and universal tensor squares
- Finite lattice representation and undecidability
- The ℓ¹-Bass conjecture for all discrete groups
- Finite symmetric tensor categories and the Verlinde tower
- Integral counterexamples to Gersten’s conjecture
- Foulkes' conjecture for sixth powers and quadratic stabilization
Probability and statistical mechanics 29 families, 19 with Lean
- The geometric phase diagram, diffusion, and spectra of random planar maps
- Planar first-passage geometry and the absence of bigeodesics
- Critical percolation on every quasi-transitive graph
- The Benjamini–Schramm nonuniqueness conjecture
- Canonical \(O(3)\) continuum limit and exact \(O(4)\) mass asymptotics
- Critical and near-critical XY scaling and BKT universality
- The low-temperature Sherrington–Kirkpatrick fluctuation law
- Conformal universality for weakly interacting and random-bond Ising models
- GOE bulk universality for regular graphs with weak Anderson disorder
- Directional zero–one laws beyond iid environments and iid ballisticity
- The Mézard–Parisi formula for diluted spin glasses
- Perceptron free energies and microscopic jamming exponents
- Random-cluster interfaces: critical, disordered, thermal, and natural-time scaling
- Critical and quenched near-critical universality for Poisson–Voronoi percolation
- Gaussian free field limits throughout the balanced six-vertex regime
- The double-dimer loop ensemble converges to CLE4
- Critical SK autocorrelation processes and dynamics across the temperature transition
- Continuum phase transitions for radial pair potentials
- Exact three- and four-state reconstruction thresholds and four-state tree capacity
- Exact Hausdorff gauges for SLE
- The free uniform spanning forest is a factor of IID
- Gaussian fields and interfaces for triangular-lattice Lipschitz heights
- The joint critical Ashkin–Teller current limit
- All-temperature pressure of orthogonally invariant Ising spin glasses
- Limiting random SAT thresholds, sharp variance and computability
- The exact factor-of-IID threshold for free Ising spins on trees
- The three-quarter exponent for honeycomb self-avoiding walk
- Optimal logarithmic mixing of the Thorp shuffle
- Sharp singularity rates for symmetric random sign matrices
Mathematical logic 6 families, all with Lean
- Shelah’s eventual categoricity and the prescribed-threshold obstruction
- Rigidity of the Turing degrees
- Single-fold Diophantine representations and undecidability under an at-most-one-solution promise
- Separating choiceless counting from polynomial time and witnessed choice
- The Partition Principle does not imply Choice
- Weak normalization implies strong normalization in pure type systems
Group theory 14 families, 12 with Lean
- Cannon’s conjecture
- An infinite finitely presented residually finite 2-group and a finitely presented nil algebra
- Thompson’s group F is nonamenable
- A finitely generated Eilenberg–Ganea counterexample
- Boone–Higman embeddings with higher finiteness
- Amenability, unitarizability, and strong Ulam stability
- A torsion-free hyperbolic group that is neither residually finite nor linear over any field
- An infinite finitely presented simple amenable group
- Classifying spaces and geometric obstructions for Artin groups
- Quasi-isometric recognition of virtually polycyclic groups
- Nonsingular systems of equations over arbitrary groups
- A hyperbolic group without a geometric CAT(0) action
- Gersten’s conjecture and virtual compact specialness of one-relator groups
- A group without fixed price
Mathematical physics 25 families, 17 with Lean
- Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions
- Localization and delocalization in the Anderson model
- Sharp finite-matrix Lieb–Thirring inequalities and all equality cases
- The ionization and generalized ionization conjectures
- Strong cosmic censorship near two-ended Kerr data
- Area laws and tensor networks for two-dimensional gapped systems
- Exactly three mutually unbiased bases in dimension six
- Positive-temperature Bose–Einstein condensation and exact quantum depletion
- The spin-one Haldane gap
- Uniform Laughlin gap and stability under bounded scalar disorder
- Threshold and positive-energy bound states of the BFSS matrix model
- Bloch’s law, its lattice correction, and the spherical magnetization law
- Entanglement without distillable secret key
- The entropy photon-number inequality
- Parity is not in QAC0
- QMA-hardness of continuum Coulomb energy
- Classical capacity of generalized amplitude damping
- Threshold repetition for entangled games
- Failure of Kohn–Sham ensemble representation
- Exact quantum factoring over a fixed finite gate set
- Unitary vertex operator algebras and conformal nets
- QAOA attains the SK optimum in the thermodynamic-first limit
- From scale symmetry to local conformal symmetry in four-dimensional QFT
- Polynomial-time unitary synthesis from a Boolean oracle
- The optimal quartic separation between randomized and quantum queries
Operator algebras 19 families, 15 with Lean
- Counterexamples to Baum–Connes and Kadison–Kaplansky
- Rigidity and arithmetic of lattice von Neumann algebras
- Isomorphism of the free group factors
- Kadison’s similarity conjecture
- Strong Kadison–Kastler stability and its spatial boundaries
- Relative bicentralizers and modular spectral recovery
- Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stability
- Kirchberg’s \(\mathcal O_2\) norm-ultrapower embedding problem
- Invariant projections, hyperinvariant subspaces, and transitive algebras
- Kaplansky’s quasitrace conjecture and failure of tensor-product stable finiteness
- The Kadison–Ringrose cohomology conjecture
- The generator problem for finite factors
- A ZFC counterexample to Naimark’s problem
- Two notions of free entropy differ even when both are finite
- The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stability
- Approximation and quadratic strong-operator paving
- Trace cones and Razak–Jacelon stabilization
- Radius of comparison equals half the mean dimension
- Weak pure infiniteness and Cuntz-algebra absorption
Topology 18 families, 3 with Lean
- The Hilbert–Smith conjecture in every dimension
- Four-dimensional disk embedding and Wall’s conjecture
- The purely cosmetic surgery conjecture
- Failure of rational injectivity for maximal coarse assembly
- Finite Smith–Toda complexes at every height
- The Kervaire invariant problem at the prime three
- Quillen’s conjecture in rational homology
- The Hovey–Strickland and Chai conjectures
- The Grothendieck homotopy hypothesis
- Finite generation for the \(K(n)\)-local sphere
- Cyclic length and chromatic fixed-point loss
- The four-dimensional Singer conjecture
- Curtis’s conjecture
- Thomason model structures in all strict higher dimensions
- Chromatic splitting: filtrations and counterexamples
- Counterexamples to finite generation at chromatic height two
- Nonhomeomorphic closed aspherical four-manifolds
- A counterexample to Wall’s finite D(2) problem
Functional analysis 11 families, 10 with Lean
- Tingley’s sphere-isometry problem
- Independence of the separable quotient problem
- Lipschitz equivalent Banach spaces need not be linearly isomorphic
- The complete Crouzeix conjecture
- The cotype–cotype conjecture under the approximation property
- Markov type characterizes superreflexivity
- Nonexpansive fixed points in reflexive Banach spaces
- A counterexample to metric-entropy duality
- A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces
- Reflexive midpoint convexity and diamond distortion
- Metric Markov cotype of ℓ1 and Hilbert-space Lipschitz extension
Differential geometry 29 families, 15 with Lean
- Smooth isometric immersions of surfaces into ℝ4
- A smooth surface metric with no local isometric immersion in ℝ3
- Gromov’s integral scalar-curvature bound for simplicial volume
- Spectral scalar curvature, Urysohn width, and macroscopic dimension
- Sharp Cartan–Hadamard isoperimetry and rigidity
- Yau’s uniformization conjecture
- Katok’s entropy rigidity conjecture
- A counterexample to the nearby Lagrangian conjecture
- Donaldson’s hypersymplectic deformation conjecture
- Donaldson’s tamed-to-compatible conjecture
- Symplectic ball packing in higher dimensions
- The metric Blaschke conjecture
- Infinitely many closed geodesics on Riemannian spheres and closed three-manifolds
- Sharp singular-set bounds for stationary integral varifolds
- Counterexamples to stable-Morse and strong Arnold fixed-point bounds
- Nonnegative-curvature Einstein classification and an L2 topological gap
- The Solomon–Yau least-volume conjecture
- Yau’s nodal bounds: surfaces and higher dimensions
- Scalar curvature and finite-time Ricci-flow singularities
- A finite-time singularity of Calabi flow
- Affine Bernstein rigidity through dimension nine and a smooth dimension-ten counterexample
- The isoperimetric profile of the cubic three-torus
- Unique tangent flows at the first surface singularity
- Gigli’s characterization of Alexandrov curvature
- Bi-Lipschitz coordinates at every regular RCD point
- A three-manifold without conjugate points or nonpositive curvature
- Negative Kähler curvature without bounded holomorphic coordinates
- Weak MTW curvature gives convexity and regular optimal transport
- Failure of integer-degree harmonic dimension comparison
Partial differential equations 16 families, 11 with Lean
- Global smoothness for relativistic Vlasov–Maxwell
- Nonuniqueness with local conservation for the hard-sphere Boltzmann equation
- Kinetic limits and fluctuations over the Boltzmann lifespan
- Joint metric and connection recovery from one boundary patch
- The planar Mumford–Shah regularity conjecture and local weak-L4 gradient bounds
- The critical dimension for the one-phase Bernoulli problem
- The three-dimensional Ball–Evans approximation problem
- The hot spots conjecture for simply connected planar domains
- The Lane–Emden and Hénon–Lane–Emden conjectures
- Stable blowup for the defocusing Schrödinger equation
- Global uniqueness in smooth isotropic elasticity
- Nonattainment of the three-marginal Coulomb Monge problem
- Sharp one-third stability of Brenier maps
- De Giorgi’s conjecture in dimension eight
- Universal computation in forced Navier–Stokes flows
- Interior \(C^{1,\alpha}\) regularity for infinity-harmonic functions
What OpenAI published
OpenAI labels 189 of the 416 Lean statement files as main results in its Lean catalogue.
The papers cite one another in 586 directed pairs and cite 11,019 works outside the release. OpenAI has withdrawn 3 papers and replaced 27 with later editions.
Atlas links public contributions credited to 371 names and places 671 reports beside the results they discuss.
Who examined the release, and how
These groups report different kinds of work: verifying a formal proof with a program, comparing a Lean statement with a paper, or testing a finite claim by calculation. Atlas links their original reports and has not repeated their work.
- Carlos Toledo, cert-machine ran Comparator on OpenAI’s proofs with a second independent verifier, tested finite claims in some papers by exact calculation, and compared the Lean statements with OpenAI’s catalogue descriptions.
- MathVet ran Comparator on OpenAI’s proofs in an isolated environment and compared the Lean statements with OpenAI’s catalogue descriptions under published assessment rules.
- Neal McBurnett, openai-math-lean-tooling ran Comparator on OpenAI’s proofs using Lean’s own proof verifier and recorded the time and memory used.
- Ben Knill, openai-math-hol-cards proved selected intermediate steps using HOL Light, a different proof assistant, and tested incorrect examples that the program should reject.
- Thomas Bloom, erdosproblems.com identifies which Erdős problems the papers address. These links do not assess whether the claimed proofs are correct.
How to help
Each contribution covers one result or one page, and is credited by name on the pages it changes.
Without an AI account
Open a short GitHub form to explain a result, compare a Lean statement with its paper, or report a problem with a page.
With an AI account
Give your assistant the start-here guide from the repository. It helps you choose one useful note, drafts it privately and leaves the signing to you.
Some Lean statements have a specific reason to be read first.See which, and why