Main Page: Difference between revisions
From OpenAI Aftermath
Probability: link the new page GOE bulk universality for random regular graphs |
Link the new page on the Partition Principle |
||
| (41 intermediate revisions by the same user not shown) | |||
| Line 9: | Line 9: | ||
== Browse == | == Browse == | ||
* [[:Category:OpenAI results|All result pages]] | * [[:Category:OpenAI results|All result pages]] | ||
* [[Results by number of public follow-ups]] (sortable overview) | |||
* Number theory: | * Number theory: | ||
** [[Milne's rationality conjecture]] | ** [[Milne's rationality conjecture]] | ||
| Line 15: | Line 16: | ||
** [[Modularity of elliptic curves over imaginary quadratic fields]] | ** [[Modularity of elliptic curves over imaginary quadratic fields]] | ||
** [[The Fontaine–Mazur conjecture at the prime 2]] | ** [[The Fontaine–Mazur conjecture at the prime 2]] | ||
** [[The p-adic section conjecture]] | |||
** [[Geometric Langlands and the generalized Ramanujan conjecture over function fields]] | ** [[Geometric Langlands and the generalized Ramanujan conjecture over function fields]] | ||
** [[The Birch and Swinnerton-Dyer formula in low Selmer corank]] | ** [[The Birch and Swinnerton-Dyer formula in low Selmer corank]] | ||
| Line 20: | Line 22: | ||
** [[The higher-dimensional Duke problem for torus packets]] | ** [[The higher-dimensional Duke problem for torus packets]] | ||
** [[The quasi-Riemann hypothesis]] | ** [[The quasi-Riemann hypothesis]] | ||
** [[Uniform exclusion of Landau–Siegel zeros]] | |||
** [[Prime-factor statistics of p − 1]] | ** [[Prime-factor statistics of p − 1]] | ||
** [[Largest prime factors of consecutive integers]] | |||
** [[Primitive roots for every admissible integer base]] | ** [[Primitive roots for every admissible integer base]] | ||
** [[Bounded gaps between primes]] | ** [[Bounded gaps between primes]] | ||
| Line 30: | Line 34: | ||
** [[Ostmann's inverse Goldbach conjecture]] | ** [[Ostmann's inverse Goldbach conjecture]] | ||
** [[The Gaussian moat problem]] | ** [[The Gaussian moat problem]] | ||
** [[The two-point Chowla conjecture]] | |||
* Algebraic geometry: | * Algebraic geometry: | ||
** [[The rational Hodge conjecture for CM abelian varieties]] | ** [[The rational Hodge conjecture for CM abelian varieties]] | ||
| Line 37: | Line 42: | ||
** [[The abelian Zilber–Pink conjecture]] | ** [[The abelian Zilber–Pink conjecture]] | ||
** [[The ordinary double point volume gap]] | ** [[The ordinary double point volume gap]] | ||
** [[The abundance conjecture for threefolds in positive characteristic]] | |||
** [[The hyperkähler SYZ conjecture]] | |||
** [[The Zariski cancellation problem over the complex numbers]] | |||
** [[The stable coordinate and Abhyankar–Sathaye conjectures]] | |||
** [[Nagata's conjecture on plane curves]] | |||
** [[Bloch's conjecture for surfaces with geometric genus zero]] | |||
** [[Zariski's multiplicity conjecture]] | |||
** [[The equivariant cohomological Hikita conjecture]] | |||
* Convex geometry: | * Convex geometry: | ||
** [[The Mahler conjectures]] | ** [[The Mahler conjectures]] | ||
** [[The logarithmic Brunn–Minkowski conjecture]] | |||
** [[Petty's projection-volume conjecture]] | |||
** [[The optimal order of convex-body covering density]] | |||
** [[The generalized Lax conjecture]] | |||
* Algebraic complexity: | * Algebraic complexity: | ||
** [[Matrix multiplication with exponent at most 9/4]] | ** [[Matrix multiplication with exponent at most 9/4]] | ||
| Line 49: | Line 66: | ||
** [[Worst-case Subset Sum below the meet-in-the-middle bound]] | ** [[Worst-case Subset Sum below the meet-in-the-middle bound]] | ||
** [[Sensitivity versus block sensitivity]] | ** [[Sensitivity versus block sensitivity]] | ||
** [[The Gotsman–Linial conjecture]] | |||
** [[Hardness of coloring three-colorable graphs]] | ** [[Hardness of coloring three-colorable graphs]] | ||
** [[The Sakoda–Sipser problem]] | |||
** [[Derandomization of logarithmic space]] | |||
** [[Moore's parity conjecture for constant-depth quantum circuits]] | |||
* Group theory: | * Group theory: | ||
** [[Classifying spaces and geometric obstructions for Artin groups]] | ** [[Classifying spaces and geometric obstructions for Artin groups]] | ||
| Line 57: | Line 78: | ||
** [[The finitely presented Burnside problem]] | ** [[The finitely presented Burnside problem]] | ||
** [[The Kervaire conjecture]] | ** [[The Kervaire conjecture]] | ||
** [[Residual finiteness of hyperbolic groups]] | |||
** [[The Boone–Higman conjecture]] | |||
** [[Gersten's conjecture and virtual specialness of one-relator groups]] | |||
* Algebra: | * Algebra: | ||
** [[The Deligne–Drinfeld conjecture]] | ** [[The Deligne–Drinfeld conjecture]] | ||
** [[Lech's multiplicity conjecture]] | ** [[Lech's multiplicity conjecture]] | ||
** [[Serre's positivity conjecture for intersection multiplicities]] | |||
** [[Foulkes' conjecture]] | ** [[Foulkes' conjecture]] | ||
** [[The Benson–Etingof–Ostrik conjecture for finite tensor categories]] | |||
** [[The Eisenbud–Green–Harris and lex-plus-powers conjectures]] | |||
** [[The combinatorial invariance conjecture for Kazhdan–Lusztig polynomials]] | |||
* Homotopy theory: | * Homotopy theory: | ||
** [[The Grothendieck homotopy hypothesis]] | ** [[The Grothendieck homotopy hypothesis]] | ||
| Line 68: | Line 96: | ||
** [[The chromatic splitting conjecture]] | ** [[The chromatic splitting conjecture]] | ||
** [[Curtis's conjecture]] | ** [[Curtis's conjecture]] | ||
** [[Wall's D(2) problem]] | |||
** [[Thomason model structures on strict higher categories]] | |||
** [[Finite generation of the homotopy of the K(n)-local sphere]] | |||
* Geometric topology: | * Geometric topology: | ||
** [[The Hilbert–Smith conjecture]] | ** [[The Hilbert–Smith conjecture]] | ||
| Line 76: | Line 107: | ||
* Mathematical logic: | * Mathematical logic: | ||
** [[Rigidity of the Turing degrees]] | ** [[Rigidity of the Turing degrees]] | ||
** [[The Barendregt–Geuvers–Klop conjecture]] | |||
** [[The Partition Principle and the Axiom of Choice]] | |||
* Algorithms: | * Algorithms: | ||
** [[A factor-two approximation for shortest common superstring]] | ** [[A factor-two approximation for shortest common superstring]] | ||
| Line 81: | Line 114: | ||
** [[Integer multiplication below n log n]] | ** [[Integer multiplication below n log n]] | ||
** [[Deterministic polynomial factorization over prime fields]] | ** [[Deterministic polynomial factorization over prime fields]] | ||
** [[Almost-linear-time maximum matching in general graphs]] | |||
** [[Approximate counting of common bases of two matroids]] | |||
** [[Approximate counting and entropy of perfect matchings]] | |||
** [[Mean-payoff games in quasipolynomial time]] | |||
** [[One-sample matroid prophet inequalities]] | |||
** [[Scheduling unit jobs with precedence constraints on three machines]] | |||
** [[Sampling and counting contingency tables]] | |||
** [[Rapid mixing of the switch chain for every degree sequence]] | |||
** [[The randomized k-server problem on arbitrary metrics]] | |||
* Combinatorics: | * Combinatorics: | ||
** [[Barnette's conjecture]] | ** [[Barnette's conjecture]] | ||
| Line 95: | Line 137: | ||
** [[Sidorenko's conjecture]] | ** [[Sidorenko's conjecture]] | ||
** [[The Harary–Hill and Zarankiewicz crossing-number conjectures]] | ** [[The Harary–Hill and Zarankiewicz crossing-number conjectures]] | ||
** [[Talagrand's expectation-threshold and discrete-convexity conjectures]] | |||
** [[The strong thin-tree conjecture]] | |||
** [[Elementary positivity of chromatic quasisymmetric functions]] | |||
** [[Superexponential growth of van der Waerden numbers]] | |||
** [[Saxl's conjecture and the tensor square conjecture]] | |||
** [[The infinite matroid intersection and packing/covering conjectures]] | |||
** [[The logarithmic exponent of off-diagonal Ramsey numbers]] | |||
* Discrete geometry: | * Discrete geometry: | ||
** [[Borsuk's conjecture]] | ** [[Borsuk's conjecture]] | ||
| Line 104: | Line 153: | ||
** [[Classification of finite Euclidean Ramsey configurations]] | ** [[Classification of finite Euclidean Ramsey configurations]] | ||
** [[Cylinder coverings below the half-area bound]] | ** [[Cylinder coverings below the half-area bound]] | ||
** [[The Euclidean Steinitz–Bergström conjecture]] | |||
** [[Heilbronn's triangle problem]] | |||
* Real analysis: | * Real analysis: | ||
** [[The Erdős similarity conjecture]] | ** [[The Erdős similarity conjecture]] | ||
** [[Singular Bernoulli convolutions]] | |||
* Complex analysis: | |||
** [[Brennan's conjecture]] | |||
** [[Kobayashi's canonical-ampleness conjecture]] | |||
** [[The Oka property of complex K3 surfaces]] | |||
* Harmonic analysis: | * Harmonic analysis: | ||
** [[Endpoint Sobolev regularity of the centered maximal function]] | ** [[Endpoint Sobolev regularity of the centered maximal function]] | ||
| Line 111: | Line 167: | ||
** [[The Falconer distance conjecture]] | ** [[The Falconer distance conjecture]] | ||
** [[The Kakeya conjecture in three and four dimensions]] | ** [[The Kakeya conjecture in three and four dimensions]] | ||
** [[Ultraflat real Littlewood polynomials]] | |||
** [[Sogge's local smoothing conjecture in three dimensions]] | |||
** [[The David–Semmes problem in higher codimension]] | |||
** [[Fourier extension for positively curved surfaces in three dimensions]] | |||
* Functional analysis: | * Functional analysis: | ||
** [[The separable quotient problem]] | ** [[The separable quotient problem]] | ||
** [[The hyperinvariant subspace problem]] | ** [[The hyperinvariant subspace problem]] | ||
** [[The Lang–Plaut problem]] | |||
** [[Metric Markov cotype of ℓ1]] | |||
** [[The complete Crouzeix conjecture]] | |||
* Partial differential equations: | * Partial differential equations: | ||
** [[The hot spots conjecture for simply connected planar domains]] | ** [[The hot spots conjecture for simply connected planar domains]] | ||
| Line 119: | Line 182: | ||
** [[De Giorgi's conjecture]] | ** [[De Giorgi's conjecture]] | ||
** [[Regularity of infinity-harmonic functions]] | ** [[Regularity of infinity-harmonic functions]] | ||
** [[The Mumford–Shah conjecture]] | |||
** [[Stable blowup for the defocusing nonlinear Schrödinger equation]] | |||
** [[Sharp Hölder stability of Brenier maps]] | |||
** [[Universal computation in forced Navier–Stokes flows]] | |||
* Operator algebras: | * Operator algebras: | ||
** [[Isomorphism of the free group factors]] | ** [[Isomorphism of the free group factors]] | ||
** [[The Toms–Winter conjecture]] | ** [[The Toms–Winter conjecture]] | ||
** [[Strong locality of unitary vertex operator algebras]] | ** [[Strong locality of unitary vertex operator algebras]] | ||
** [[Connes' bicentralizer problem]] | |||
** [[Naimark's problem]] | |||
** [[The Phillips–Toms conjecture]] | |||
** [[The generator problem for von Neumann algebras]] | |||
* Differential geometry: | * Differential geometry: | ||
** [[Smooth isometric immersions of surfaces into four-space]] | ** [[Smooth isometric immersions of surfaces into four-space]] | ||
| Line 129: | Line 200: | ||
** [[The Solomon–Yau least-volume conjecture]] | ** [[The Solomon–Yau least-volume conjecture]] | ||
** [[The Gromov–Lawson aspherical conjecture]] | ** [[The Gromov–Lawson aspherical conjecture]] | ||
** [[Finite-time singularities of Calabi flow]] | |||
** [[The LeBrun–Salamon conjecture]] | |||
** [[The Cartan–Hadamard isoperimetric conjecture]] | |||
** [[Positively curved Einstein four-manifolds]] | |||
** [[Yau's uniformization conjecture]] | |||
** [[Strong forms of the Arnold conjecture]] | |||
** [[The affine Bernstein problem]] | |||
** [[Infinitely many closed geodesics on Riemannian spheres]] | |||
** [[Donaldson's tamed-to-compatible conjecture]] | |||
* Mathematical physics: | * Mathematical physics: | ||
** [[Mass generation in two-dimensional O(n) models]] | ** [[Mass generation in two-dimensional O(n) models]] | ||
** [[ | ** [[Pure-point spectrum of the two-dimensional Anderson model]] | ||
** [[Absolutely continuous spectrum of the Anderson model in dimension at least three]] | |||
** [[Bose–Einstein condensation in the dilute Bose gas]] | ** [[Bose–Einstein condensation in the dilute Bose gas]] | ||
** [[The area law for gapped ground states in two dimensions]] | ** [[The area law for gapped ground states in two dimensions]] | ||
| Line 138: | Line 219: | ||
** [[The ionization and generalized ionization conjectures]] | ** [[The ionization and generalized ionization conjectures]] | ||
** [[Bound states of the BFSS matrix model]] | ** [[Bound states of the BFSS matrix model]] | ||
** [[The one-dimensional Lieb–Thirring conjecture]] | |||
* Quantum information: | * Quantum information: | ||
** [[Classical capacity of generalized amplitude damping]] | ** [[Classical capacity of generalized amplitude damping]] | ||
** [[Mutually unbiased bases in dimension six]] | ** [[Mutually unbiased bases in dimension six]] | ||
** [[Threshold parallel repetition for entangled games]] | |||
** [[Entanglement without secret key and the PPT-squared conjecture]] | |||
* Information theory: | * Information theory: | ||
** [[The Courtade–Kumar conjecture]] | ** [[The Courtade–Kumar conjecture]] | ||
| Line 153: | Line 237: | ||
** [[Scaling limits of critical Fortuin–Kasteleyn planar maps]] | ** [[Scaling limits of critical Fortuin–Kasteleyn planar maps]] | ||
** [[The low-temperature Sherrington–Kirkpatrick fluctuation law]] | ** [[The low-temperature Sherrington–Kirkpatrick fluctuation law]] | ||
** [[Glauber dynamics of the Sherrington–Kirkpatrick model]] | |||
** [[GOE bulk universality for random regular graphs]] | ** [[GOE bulk universality for random regular graphs]] | ||
** [[The second Kahn–Kalai conjecture]] | |||
** [[Bigeodesics in planar first-passage percolation]] | |||
* Dynamical systems: | * Dynamical systems: | ||
** [[Uniform bounds for limit cycles in Hilbert's sixteenth problem]] | ** [[Uniform bounds for limit cycles in Hilbert's sixteenth problem]] | ||
** [[Permanence of weakly reversible mass-action systems]] | ** [[Permanence of weakly reversible mass-action systems]] | ||
** [[The near-boundary Birkhoff conjecture]] | |||
** [[Rokhlin's multiple-mixing problem]] | |||
== Collection-wide checks == | == Collection-wide checks == | ||
Latest revision as of 13:16, 20 October 2026
OpenAI Aftermath is a guide to mathematical research published by OpenAI and to publicly available follow-up work by others: extensions, applications, formal verifications, corrections and critiques.
How entries are written
- Each result page summarizes the published claim and cites its public source: the paper, the repository commit or the preprint version.
- Follow-up work is listed with its relation to the original result (extension, use, verification, correction or critique), its public date and its public status.
- The publication of a paper, code or a formal proof is reported as such. It is not presented as independent verification.
Browse
- All result pages
- Results by number of public follow-ups (sortable overview)
- Number theory:
- Milne's rationality conjecture
- Irrationality of Catalan's constant
- The irrationality exponent of π is 2
- Modularity of elliptic curves over imaginary quadratic fields
- The Fontaine–Mazur conjecture at the prime 2
- The p-adic section conjecture
- Geometric Langlands and the generalized Ramanujan conjecture over function fields
- The Birch and Swinnerton-Dyer formula in low Selmer corank
- Goldfeld's conjecture for quadratic twists
- The higher-dimensional Duke problem for torus packets
- The quasi-Riemann hypothesis
- Uniform exclusion of Landau–Siegel zeros
- Prime-factor statistics of p − 1
- Largest prime factors of consecutive integers
- Primitive roots for every admissible integer base
- Bounded gaps between primes
- Long gaps between primes
- Positive lower density of large prime gaps
- A quadratic bound for Jacobsthal's function
- The inhomogeneous Duffin–Schaeffer conjecture
- Hilbert's tenth problem over the rational numbers
- Ostmann's inverse Goldbach conjecture
- The Gaussian moat problem
- The two-point Chowla conjecture
- Algebraic geometry:
- The rational Hodge conjecture for CM abelian varieties
- Griffiths' positivity conjecture
- The Kollár–Pardon conjecture on semialgebraic universal covers
- Anticanonical nonvanishing under smooth semipositivity
- The abelian Zilber–Pink conjecture
- The ordinary double point volume gap
- The abundance conjecture for threefolds in positive characteristic
- The hyperkähler SYZ conjecture
- The Zariski cancellation problem over the complex numbers
- The stable coordinate and Abhyankar–Sathaye conjectures
- Nagata's conjecture on plane curves
- Bloch's conjecture for surfaces with geometric genus zero
- Zariski's multiplicity conjecture
- The equivariant cohomological Hikita conjecture
- Convex geometry:
- Algebraic complexity:
- Computational complexity:
- The Unique Games Conjecture
- The 2-to-1 Games Conjecture
- The existential theory of the reals in the counting hierarchy
- Worst-case Subset Sum below the meet-in-the-middle bound
- Sensitivity versus block sensitivity
- The Gotsman–Linial conjecture
- Hardness of coloring three-colorable graphs
- The Sakoda–Sipser problem
- Derandomization of logarithmic space
- Moore's parity conjecture for constant-depth quantum circuits
- Group theory:
- Classifying spaces and geometric obstructions for Artin groups
- Thompson's group F is nonamenable
- Kaplansky's zero-divisor conjecture
- Kaplansky's direct-finiteness conjecture
- The finitely presented Burnside problem
- The Kervaire conjecture
- Residual finiteness of hyperbolic groups
- The Boone–Higman conjecture
- Gersten's conjecture and virtual specialness of one-relator groups
- Algebra:
- The Deligne–Drinfeld conjecture
- Lech's multiplicity conjecture
- Serre's positivity conjecture for intersection multiplicities
- Foulkes' conjecture
- The Benson–Etingof–Ostrik conjecture for finite tensor categories
- The Eisenbud–Green–Harris and lex-plus-powers conjectures
- The combinatorial invariance conjecture for Kazhdan–Lusztig polynomials
- Homotopy theory:
- The Grothendieck homotopy hypothesis
- Smith–Toda complexes at every height
- The Kervaire invariant problem at the prime three
- The Hovey–Strickland conjecture
- The chromatic splitting conjecture
- Curtis's conjecture
- Wall's D(2) problem
- Thomason model structures on strict higher categories
- Finite generation of the homotopy of the K(n)-local sphere
- Geometric topology:
- Representation theory of algebras:
- Mathematical logic:
- Algorithms:
- A factor-two approximation for shortest common superstring
- Exact Fourier transforms below n log n
- Integer multiplication below n log n
- Deterministic polynomial factorization over prime fields
- Almost-linear-time maximum matching in general graphs
- Approximate counting of common bases of two matroids
- Approximate counting and entropy of perfect matchings
- Mean-payoff games in quasipolynomial time
- One-sample matroid prophet inequalities
- Scheduling unit jobs with precedence constraints on three machines
- Sampling and counting contingency tables
- Rapid mixing of the switch chain for every degree sequence
- The randomized k-server problem on arbitrary metrics
- Combinatorics:
- Barnette's conjecture
- Hadwiger's conjecture
- Monochromatic finite sums and products in the positive integers
- The hypercube Ramsey number has linear order
- The cycle–clique Ramsey conjecture
- The Erdős–Gallai cycle-decomposition conjecture
- Power-saving bounds for square-difference-free sets
- Polynomial removal for ordered binary matrices
- The sharp constant in random triangle removal
- Seymour's second-neighborhood conjecture
- The Ajtai–Erdős–Komlós–Szemerédi independence conjecture
- Sidorenko's conjecture
- The Harary–Hill and Zarankiewicz crossing-number conjectures
- Talagrand's expectation-threshold and discrete-convexity conjectures
- The strong thin-tree conjecture
- Elementary positivity of chromatic quasisymmetric functions
- Superexponential growth of van der Waerden numbers
- Saxl's conjecture and the tensor square conjecture
- The infinite matroid intersection and packing/covering conjectures
- The logarithmic exponent of off-diagonal Ramsey numbers
- Discrete geometry:
- Borsuk's conjecture
- The periodic tiling conjecture in dimension three
- The higher-dimensional Erdős distinct-distances conjecture
- The Erdős unit distance and pinned distance problems
- The Euclidean plane is not five-colorable
- Universal optimality of the triangular lattice
- Classification of finite Euclidean Ramsey configurations
- Cylinder coverings below the half-area bound
- The Euclidean Steinitz–Bergström conjecture
- Heilbronn's triangle problem
- Real analysis:
- Complex analysis:
- Harmonic analysis:
- Endpoint Sobolev regularity of the centered maximal function
- The triangular Hilbert transform at the symmetric point
- The Falconer distance conjecture
- The Kakeya conjecture in three and four dimensions
- Ultraflat real Littlewood polynomials
- Sogge's local smoothing conjecture in three dimensions
- The David–Semmes problem in higher codimension
- Fourier extension for positively curved surfaces in three dimensions
- Functional analysis:
- Partial differential equations:
- The hot spots conjecture for simply connected planar domains
- The critical dimension for one-phase Bernoulli minimizers
- De Giorgi's conjecture
- Regularity of infinity-harmonic functions
- The Mumford–Shah conjecture
- Stable blowup for the defocusing nonlinear Schrödinger equation
- Sharp Hölder stability of Brenier maps
- Universal computation in forced Navier–Stokes flows
- Operator algebras:
- Differential geometry:
- Smooth isometric immersions of surfaces into four-space
- Spacetime Penrose inequalities
- Bi-Lipschitz charts at regular points of RCD spaces
- The Solomon–Yau least-volume conjecture
- The Gromov–Lawson aspherical conjecture
- Finite-time singularities of Calabi flow
- The LeBrun–Salamon conjecture
- The Cartan–Hadamard isoperimetric conjecture
- Positively curved Einstein four-manifolds
- Yau's uniformization conjecture
- Strong forms of the Arnold conjecture
- The affine Bernstein problem
- Infinitely many closed geodesics on Riemannian spheres
- Donaldson's tamed-to-compatible conjecture
- Mathematical physics:
- Mass generation in two-dimensional O(n) models
- Pure-point spectrum of the two-dimensional Anderson model
- Absolutely continuous spectrum of the Anderson model in dimension at least three
- Bose–Einstein condensation in the dilute Bose gas
- The area law for gapped ground states in two dimensions
- The spin-one Haldane gap
- The Laughlin spectral gap
- The ionization and generalized ionization conjectures
- Bound states of the BFSS matrix model
- The one-dimensional Lieb–Thirring conjecture
- Quantum information:
- Information theory:
- Probability:
- The Benjamini–Schramm percolation conjectures
- Free energies of random perceptrons
- Optimal mixing of the Thorp shuffle
- The random k-SAT satisfiability threshold
- An exact Hausdorff gauge for SLE
- Conformal invariance of square-lattice random-cluster interfaces
- Reconstruction thresholds for Potts broadcasting on trees
- Scaling limits of critical Fortuin–Kasteleyn planar maps
- The low-temperature Sherrington–Kirkpatrick fluctuation law
- Glauber dynamics of the Sherrington–Kirkpatrick model
- GOE bulk universality for random regular graphs
- The second Kahn–Kalai conjecture
- Bigeodesics in planar first-passage percolation
- Dynamical systems:
Collection-wide checks
- Formal-statement review. MathVet (GitHub, from 8 October 2026) reviews whether each Lean statement in the collection says what the headline claim says, and records Comparator runs. It states that it does not claim any theorem false.
- Second-kernel replay. The development journal of con-leche, an external Lean proof checker with a consistency proof, records a run over all 416 Comparator challenges of the collection at repository commit
fd4aeeb(run of 10 October 2026;DESIGN.md, tasks #348 and #352–#354). Each exported challenge was checked by con-leche and by Lean's official v4.34.1 kernel, with a one-hour time limit and a 25 GB memory limit. Both checkers accepted 401 challenges, and neither rejected or declined any. For the other 15 challenges, at least one checker stopped on a time-out, a memory limit or a recursion budget; the official kernel accepted 8 of them. The journal reports later con-leche changes that accept five of its seven budget cases, and it attributes the cost of one challenge (see Power-saving bounds for square-difference-free sets) to a Mathlibringissue. - Audit of the manuscripts without Lean. JJardine919/openai-math-audit (Lattice24; archived at Zenodo 10.5281/zenodo.23422995) reports a referee-style review, by AI review agents with independent refutation passes for major findings, of all 547 manuscripts in the collection that have no Lean formalization, completed on 16 October 2026. It reports no gap found in 544 of them, a critical gap in the holomorphicity proof of Square-lattice FK interfaces and nested loops for 1 ≤ q < 4 (inherited by one dependent manuscript; see Conformal invariance of square-lattice random-cluster interfaces), and a verifiability gap in The maximum number of mutually unbiased bases in dimension six, whose computer proof cites code and run records that are not in the public release. Every review is published, and the audit invites corrections through repository issues.
Sources
- OpenAI mathematics collection: github.com/openai/math
- OpenAI's abridged reasoning summaries for ten results: reasoning_traces (list in the repository's README)
