An index of the openai/math collection: 372 result families across 17 areas of mathematics, 162 with Lean-formalized main results.
Looking for a word inside the papers? Search the LaTeX source →
The green Lean checkmark marks the 162 papers listed in
lean/formalization.yaml,
for which OpenAI claims a Lean formalization of the main result. This index
reports that claim as listed upstream; it does not build or check the Lean code.
For a comparison of the Lean statements with the theorems in the papers, see
“Do
the Lean statements in openai/math match their papers?” (PDF, shared on the Lean Zulip).
L-functions, elliptic curves, Diophantine problems, Galois theory
58 papers31 families7 in Lean
Birational geometry, Hodge theory, moduli, enumerative invariants
89 papers36 families7 in Lean
Harmonic analysis, approximation, special functions, several complex variables
26 papers16 families7 in Lean
Convex bodies, isoperimetry, packings, metric embeddings
30 papers15 families13 in Lean
Complexity, algorithms, hardness of approximation, information theory
73 papers40 families29 in Lean
Ergodic theory, smooth dynamics, entropy, rigidity
19 papers12 families2 in Lean
Extremal and additive combinatorics, Ramsey theory, graphs, matroids
50 papers37 families19 in Lean
Commutative algebra, representation theory, rings and modules
29 papers18 families10 in Lean
Random structures, spin glasses, percolation, random matrices
105 papers29 families11 in Lean
Set theory, model theory, computability
8 papers6 families5 in Lean
Geometric group theory, Artin groups, finite and profinite groups
22 papers14 families8 in Lean
Quantum spin systems, kinetic theory, integrable systems
59 papers25 families7 in Lean
von Neumann algebras, C*-algebras, free probability
31 papers19 families6 in Lean
Low-dimensional topology, manifolds, homotopy theory
26 papers18 families1 in Lean
Banach spaces, operator theory, spectral theory
19 papers11 families16 in Lean
Curvature, Kähler geometry, minimal surfaces, symplectic geometry
49 papers29 families11 in Lean
Fluids, elliptic and dispersive equations, regularity
29 papers16 families3 in Lean
We give a negative answer to Wall's finite \(D(2)\) problem. We construct a finite connected three-dimensional CW complex satisfying the \(D(2)\) finiteness condition but not homotopy equivalent to any finite CW complex of dimension at most two. The example has infinite fundamental group.
We prove that the unit-speed billiard flow in every nondegenerate Euclidean triangle with at least one angle irrational relative to π is weakly mixing for normalized Liouville measure. Equivalently, the product of the flow with itself is ergodic.
We prove that full ordinary descendant Virasoro constraints pass from a smooth projective complex base to the projectivization of any algebraic vector bundle of rank at least two. The bundle need not split and satisfies no positivity requirement. Assuming the full constraints on the base, the conclusion includes every genus, each individual integral curve class, and all cohomology insertions, including primitive and odd classes. The result also applies successively to towers of projective bundles.
We prove joint functional convergence of the stationary and quench autocorrelations of zero-field Sherrington–Kirkpatrick heat-bath dynamics at inverse temperature β = 1, with the same random limit for Gaussian and Rademacher couplings. Each site has a rate-one clock, mean spin autocorrelations are multiplied by n1/3, and waiting times and lags are measured in units n2/3. The quench starts from independent fair spins, and convergence is uniform on compact sets of positive waiting times and lags. The quench limit is selected by these initial states and relaxes to the stationary limiting autocorrelation as the waiting time tends to infinity.
We give a uniform algorithm that reconstructs every binary string from independent deletion traces when its length and rational retention probability are known. For each fixed retention probability, both the number of traces and the bit complexity are quasipolynomial in the string length. More generally, we give an explicit sample bound uniform over all rational retention probabilities, with running time polynomial in the sample budget and the binary input length. If the deletion probability is at most \(n^{-\varepsilon}\) for fixed ε > 0, the sample and running-time bounds are polynomial. Reconstruction succeeds with probability at least 2/3 for each input string.
We prove a uniform index theorem for connected projective semi-log-canonical log Calabi–Yau pairs in every fixed dimension at least four over an algebraically closed field of characteristic zero. For boundary coefficients in a fixed finite rational set, a single multiple of the log canonical divisor is Cartier and linearly trivial. The multiple depends only on the dimension and coefficient set, not on the number of irreducible components. Together with the established theorem in dimensions at most three, this resolves the finite-rational-coefficient semi-log-canonical index conjecture.