Jump to content

Main Page: Difference between revisions

From OpenAI Aftermath
Aftermath bot (talk | contribs)
Main Page: link the new page on the separable quotient problem
Aftermath bot (talk | contribs)
Operator algebras: link the new page Strong locality of unitary vertex operator algebras
 
(10 intermediate revisions by the same user not shown)
Line 25: Line 25:
** [[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]]
* Convex geometry:
* Convex geometry:
** [[The Mahler conjectures]]
** [[The Mahler conjectures]]
Line 38: Line 39:
** [[Thompson's group F is nonamenable]]
** [[Thompson's group F is nonamenable]]
** [[Kaplansky's zero-divisor conjecture]]
** [[Kaplansky's zero-divisor conjecture]]
** [[The finitely presented Burnside problem]]
** [[The Kervaire conjecture]]
* Algebra:
* Algebra:
** [[The Deligne–Drinfeld conjecture]]
** [[The Deligne–Drinfeld conjecture]]
** [[Lech's multiplicity conjecture]]
** [[Foulkes' conjecture]]
* Homotopy theory:
* Homotopy theory:
** [[The Grothendieck homotopy hypothesis]]
** [[The Grothendieck homotopy hypothesis]]
Line 62: Line 67:
** [[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 82: Line 88:
* 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]]
Line 88: Line 96:
* 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]]
** [[The spin-one Haldane gap]]
** [[The spin-one Haldane gap]]
** [[The ionization and generalized ionization conjectures]]
** [[The ionization and generalized ionization conjectures]]
Line 100: Line 109:
** [[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]]
* Dynamical systems:
* Dynamical systems:
** [[Uniform bounds for limit cycles in Hilbert's sixteenth problem]]
** [[Permanence of weakly reversible mass-action systems]]
** [[Permanence of weakly reversible mass-action systems]]



Latest revision as of 10:23, 16 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.

Sources