Jump to content

Main Page: Difference between revisions

From OpenAI Aftermath
Aftermath bot (talk | contribs)
Main Page: add The Kollár–Pardon conjecture on semialgebraic universal covers under Algebraic geometry
Aftermath bot (talk | contribs)
Add the centered maximal function page under Harmonic analysis
 
(31 intermediate revisions by the same user not shown)
Line 14: Line 14:
** [[The irrationality exponent of π is 2]]
** [[The irrationality exponent of π is 2]]
** [[Modularity of elliptic curves over imaginary quadratic fields]]
** [[Modularity of elliptic curves over imaginary quadratic fields]]
** [[The Fontaine–Mazur conjecture at the prime 2]]
** [[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]]
** [[The quasi-Riemann hypothesis]]
** [[Prime-factor statistics of p − 1]]
** [[Prime-factor statistics of p − 1]]
Line 20: Line 25:
** [[Long gaps between primes]]
** [[Long gaps between primes]]
** [[Positive lower density of large prime gaps]]
** [[Positive lower density of large prime gaps]]
** [[A quadratic bound for Jacobsthal's function]]
** [[The inhomogeneous Duffin–Schaeffer conjecture]]
** [[The inhomogeneous Duffin–Schaeffer conjecture]]
** [[Hilbert's tenth problem over the rational numbers]]
** [[Hilbert's tenth problem over the rational numbers]]
** [[Ostmann's inverse Goldbach conjecture]]
** [[The Gaussian moat problem]]
* Algebraic geometry:
* Algebraic geometry:
** [[The rational Hodge conjecture for CM abelian varieties]]
** [[The rational Hodge conjecture for CM abelian varieties]]
** [[Griffiths' positivity conjecture]]
** [[Griffiths' positivity conjecture]]
** [[The Kollár–Pardon conjecture on semialgebraic universal covers]]
** [[The Kollár–Pardon conjecture on semialgebraic universal covers]]
** [[Anticanonical nonvanishing under smooth semipositivity]]
** [[The abelian Zilber–Pink conjecture]]
* Convex geometry:
* Convex geometry:
** [[The Mahler conjectures]]
** [[The Mahler conjectures]]
Line 35: Line 45:
** [[The existential theory of the reals in the counting hierarchy]]
** [[The existential theory of the reals in the counting hierarchy]]
** [[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]]
* Group theory:
* Group theory:
** [[Classifying spaces and geometric obstructions for Artin groups]]
** [[Classifying spaces and geometric obstructions for Artin groups]]
Line 44: Line 55:
** [[The Deligne–Drinfeld conjecture]]
** [[The Deligne–Drinfeld conjecture]]
** [[Lech's multiplicity conjecture]]
** [[Lech's multiplicity conjecture]]
** [[Foulkes' conjecture]]
* Homotopy theory:
* Homotopy theory:
** [[The Grothendieck homotopy hypothesis]]
** [[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]]
* Geometric topology:
* Geometric topology:
** [[The Hilbert–Smith conjecture]]
** [[The Hilbert–Smith conjecture]]
Line 56: Line 73:
** [[Exact Fourier transforms below n log n]]
** [[Exact Fourier transforms below n log n]]
** [[Integer multiplication below n log n]]
** [[Integer multiplication below n log n]]
** [[Deterministic polynomial factorization over prime fields]]
* Combinatorics:
* Combinatorics:
** [[Barnette's conjecture]]
** [[Barnette's conjecture]]
Line 61: Line 79:
** [[Monochromatic finite sums and products in the positive integers]]
** [[Monochromatic finite sums and products in the positive integers]]
** [[The hypercube Ramsey number has linear order]]
** [[The hypercube Ramsey number has linear order]]
** [[The cycle–clique Ramsey conjecture]]
** [[The Erdős–Gallai cycle-decomposition conjecture]]
** [[The Erdős–Gallai cycle-decomposition conjecture]]
** [[Power-saving bounds for square-difference-free sets]]
** [[Power-saving bounds for square-difference-free sets]]
Line 66: Line 85:
** [[The sharp constant in random triangle removal]]
** [[The sharp constant in random triangle removal]]
** [[Seymour's second-neighborhood conjecture]]
** [[Seymour's second-neighborhood conjecture]]
** [[The Ajtai–Erdős–Komlós–Szemerédi independence conjecture]]
* Discrete geometry:
* Discrete geometry:
** [[Borsuk's conjecture]]
** [[Borsuk's conjecture]]
Line 77: Line 97:
** [[The Erdős similarity conjecture]]
** [[The Erdős similarity conjecture]]
* Harmonic analysis:
* Harmonic analysis:
** [[Endpoint Sobolev regularity of the centered maximal function]]
** [[The triangular Hilbert transform at the symmetric point]]
** [[The triangular Hilbert transform at the symmetric point]]
** [[The Falconer distance conjecture]]
** [[The Falconer distance conjecture]]
** [[The Kakeya conjecture in three and four dimensions]]
* Functional analysis:
* Functional analysis:
** [[The separable quotient problem]]
** [[The separable quotient problem]]
Line 86: Line 108:
* Operator algebras:
* Operator algebras:
** [[Isomorphism of the free group factors]]
** [[Isomorphism of the free group factors]]
** [[The Toms–Winter conjecture]]
** [[Strong locality of unitary vertex operator algebras]]
* Differential geometry:
* Differential geometry:
** [[Smooth isometric immersions of surfaces into four-space]]
** [[Smooth isometric immersions of surfaces into four-space]]
** [[Spacetime Penrose inequalities]]
** [[Spacetime Penrose inequalities]]
** [[Bi-Lipschitz charts at regular points of RCD spaces]]
** [[The Solomon–Yau least-volume conjecture]]
** [[The Solomon–Yau least-volume conjecture]]
* Mathematical physics:
* Mathematical physics:
** [[Localization and delocalization in the Anderson model]]
** [[Localization and delocalization in the Anderson model]]
** [[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 spin-one Haldane gap]]
** [[The spin-one Haldane gap]]
** [[The Laughlin spectral gap]]
** [[The ionization and generalized ionization conjectures]]
** [[The ionization and generalized ionization conjectures]]
* Quantum information:
* Quantum information:
** [[Classical capacity of generalized amplitude damping]]
** [[Classical capacity of generalized amplitude damping]]
** [[Mutually unbiased bases in dimension six]]
* Information theory:
* Information theory:
** [[The Courtade–Kumar conjecture]]
** [[The Courtade–Kumar conjecture]]
Line 105: Line 133:
** [[An exact Hausdorff gauge for SLE]]
** [[An exact Hausdorff gauge for SLE]]
** [[Conformal invariance of square-lattice random-cluster interfaces]]
** [[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]]
* Dynamical systems:
* Dynamical systems:
** [[Uniform bounds for limit cycles in Hilbert's sixteenth problem]]
** [[Uniform bounds for limit cycles in Hilbert's sixteenth problem]]
Line 112: Line 143:
* '''Formal-statement review.''' [https://github.com/mathvet/mathvet 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.
* '''Formal-statement review.''' [https://github.com/mathvet/mathvet 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 [https://github.com/leanprover/con-leche 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 <code>fd4aeeb</code> (run of 10 October 2026; [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md <code>DESIGN.md</code>], 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 Mathlib <code>ring</code> issue.
* '''Second-kernel replay.''' The development journal of [https://github.com/leanprover/con-leche 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 <code>fd4aeeb</code> (run of 10 October 2026; [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md <code>DESIGN.md</code>], 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 Mathlib <code>ring</code> issue.
* '''Audit of the manuscripts without Lean.''' [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (Lattice24; archived at [https://doi.org/10.5281/zenodo.23422995 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 ==
== Sources ==
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]
* OpenAI's abridged reasoning summaries for ten results: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/reasoning_traces reasoning_traces] (list in the repository's [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md README])
* OpenAI's abridged reasoning summaries for ten results: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/reasoning_traces reasoning_traces] (list in the repository's [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md README])

Latest revision as of 13:49, 17 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

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 Mathlib ring issue.
  • 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