Main Page: Difference between revisions
Appearance
Browse: add The Hilbert–Smith conjecture (Geometric topology) |
Browse: add The sharp constant in random triangle removal, Isomorphism of the free group factors (new heading Operator algebras), Spacetime Penrose inequalities |
||
| (2 intermediate revisions by the same user not shown) | |||
| Line 57: | Line 57: | ||
** [[Power-saving bounds for square-difference-free sets]] | ** [[Power-saving bounds for square-difference-free sets]] | ||
** [[Polynomial removal for ordered binary matrices]] | ** [[Polynomial removal for ordered binary matrices]] | ||
** [[The sharp constant in random triangle removal]] | |||
* Discrete geometry: | * Discrete geometry: | ||
** [[Borsuk's conjecture]] | ** [[Borsuk's conjecture]] | ||
| Line 64: | Line 65: | ||
** [[Universal optimality of the triangular lattice]] | ** [[Universal optimality of the triangular lattice]] | ||
** [[Classification of finite Euclidean Ramsey configurations]] | ** [[Classification of finite Euclidean Ramsey configurations]] | ||
** [[Cylinder coverings below the half-area bound]] | |||
* Real analysis: | * Real analysis: | ||
** [[The Erdős similarity conjecture]] | ** [[The Erdős similarity conjecture]] | ||
| Line 71: | Line 73: | ||
** [[The hot spots conjecture for simply connected planar domains]] | ** [[The hot spots conjecture for simply connected planar domains]] | ||
** [[The critical dimension for one-phase Bernoulli minimizers]] | ** [[The critical dimension for one-phase Bernoulli minimizers]] | ||
* Operator algebras: | |||
** [[Isomorphism of the free group factors]] | |||
* Differential geometry: | * Differential geometry: | ||
** [[Smooth isometric immersions of surfaces into four-space]] | ** [[Smooth isometric immersions of surfaces into four-space]] | ||
** [[Spacetime Penrose inequalities]] | |||
* Mathematical physics: | * Mathematical physics: | ||
** [[Localization and delocalization in the Anderson model]] | ** [[Localization and delocalization in the Anderson model]] | ||
| Line 89: | Line 94: | ||
* Dynamical systems: | * Dynamical systems: | ||
** [[Permanence of weakly reversible mass-action systems]] | ** [[Permanence of weakly reversible mass-action systems]] | ||
== Collection-wide checks == | |||
* '''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. | |||
== 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 17:22, 15 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
- 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 quasi-Riemann hypothesis
- Prime-factor statistics of p − 1
- Primitive roots for every admissible integer base
- Bounded gaps between primes
- Long gaps between primes
- The inhomogeneous Duffin–Schaeffer conjecture
- Algebraic geometry:
- Convex geometry:
- Algebraic complexity:
- Computational complexity:
- Group theory:
- Algebra:
- Homotopy theory:
- Geometric topology:
- Representation theory of algebras:
- Mathematical logic:
- Algorithms:
- Combinatorics:
- Barnette's conjecture
- Hadwiger's conjecture
- Monochromatic finite sums and products in the positive integers
- The hypercube Ramsey number has linear order
- 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
- Discrete geometry:
- Borsuk's conjecture
- The periodic tiling conjecture in dimension three
- The higher-dimensional Erdős distinct-distances conjecture
- 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
- Real analysis:
- Harmonic analysis:
- Partial differential equations:
- Operator algebras:
- Differential geometry:
- Mathematical physics:
- Quantum information:
- Information theory:
- Probability:
- 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.
Sources
- OpenAI mathematics collection: github.com/openai/math
- OpenAI's abridged reasoning summaries for ten results: reasoning_traces (list in the repository's README)