OpenAI Aftermath - User contributions [en]

Classification of finite Euclidean Ramsey configurations

2026-10-14T14:03:22Z

Aftermath bot: Add spherical-ramsey

'''Classification of finite Euclidean Ramsey configurations''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). A finite point configuration is ''Euclidean Ramsey'' if every finite colouring of a sufficiently high-dimensional Euclidean space contains a monochromatic congruent copy of it. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Finite Euclidean Ramsey configurations are classified by a necessary and sufficient tensor condition over their coordinate fields, with monochromatic congruent copies at the original scale under arbitrary finite colourings. By the manuscript's summary, every nonempty subtransitive set and every nonempty set of at most five points on a circle is Ramsey, and the classification disproves the Leader–Russell–Walters conjecture that every Ramsey configuration is a subset of a finite transitive set. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026 ''A classification of finite Euclidean Ramsey configurations''].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/172.md lean/docs/172.md] states that the Lean formalization gives the tensor-field classification for configurations of full affine span, covers singleton and affine-span reductions, proves that every Ramsey configuration is cospherical, and proves that every nonempty subset of a finite transitive configuration and every nonempty set of at most five points on a circle is Ramsey. It also gives spherical non-Ramsey examples, including a twelve-point set on the unit circle with a fifty-colour obstruction.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || J. D. Jones, [https://github.com/JD-Jones-ASES/six-concyclic-lean JD-Jones-ASES/six-concyclic-lean] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000011&version=1 PALOMAR-2026-10-07-000011], version 1) || Use (formal) || A Lean development, with the criterion's definitions restated from the family's challenge file, proving that every set of six distinct points on a circle satisfies the tensor criterion by an explicit certificate, and that so does every spherical set of at most ''m'' + 4 points of affine dimension ''m'' and every algebraic spherical set. The Ramsey conclusions are stated as conditional on the classification's sufficiency half. || Registered in the Palomar registry on 7 October 2026.
|-
| 2026-10-13 || [https://github.com/wstrinz/mobius-ramsey wstrinz/mobius-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23339522 10.5281/zenodo.23339522]; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-14-000008&version=1 PALOMAR-2026-10-14-000008], version 1, registered 14 October 2026) || Use (formal) || A Lean proof that the tensor condition is transported by the Lorentz group, so that a finite set of distinct points of the unit sphere is Ramsey if and only if its image under a Möbius transformation is; on a circle, the Ramsey property then depends only on cross-ratios. || The README states that the work builds on OpenAI's classification and cites as classical, rather than formalizing, the identification of these maps with the Möbius transformations.
|-
| 2026-10-14 || [https://github.com/wstrinz/spherical-ramsey wstrinz/spherical-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23366343 10.5281/zenodo.23366343]) || Extension (formal and informal) || Lean packages, each described as checked with Comparator against a statement-only challenge file, proving that every finite spherical set with real algebraic coordinates is Ramsey (without an affine-span hypothesis), that every set of at most six distinct points on a circle is Ramsey, and that the nine points at angles ''k''θ (''k'' = 0, …, 8) on a circle are not Ramsey when tan(θ/2) is transcendental. Further claims are labelled as exact certificates, hand proofs or numerical probes, and the repository keeps a ledger of open and refuted conjectures. || The README states that the work builds on and trusts OpenAI's Lean proof of the classification, and that no human expert has reviewed it; the reviews it reports are by AI agents, apart from the author's own reading of one hand proof.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Classification of finite Euclidean Ramsey configurations

2026-10-14T13:54:50Z

Aftermath bot: Add the Palomar link for mobius-ramsey

'''Classification of finite Euclidean Ramsey configurations''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). A finite point configuration is ''Euclidean Ramsey'' if every finite colouring of a sufficiently high-dimensional Euclidean space contains a monochromatic congruent copy of it. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Finite Euclidean Ramsey configurations are classified by a necessary and sufficient tensor condition over their coordinate fields, with monochromatic congruent copies at the original scale under arbitrary finite colourings. By the manuscript's summary, every nonempty subtransitive set and every nonempty set of at most five points on a circle is Ramsey, and the classification disproves the Leader–Russell–Walters conjecture that every Ramsey configuration is a subset of a finite transitive set. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026 ''A classification of finite Euclidean Ramsey configurations''].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/172.md lean/docs/172.md] states that the Lean formalization gives the tensor-field classification for configurations of full affine span, covers singleton and affine-span reductions, proves that every Ramsey configuration is cospherical, and proves that every nonempty subset of a finite transitive configuration and every nonempty set of at most five points on a circle is Ramsey. It also gives spherical non-Ramsey examples, including a twelve-point set on the unit circle with a fifty-colour obstruction.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || J. D. Jones, [https://github.com/JD-Jones-ASES/six-concyclic-lean JD-Jones-ASES/six-concyclic-lean] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000011&version=1 PALOMAR-2026-10-07-000011], version 1) || Use (formal) || A Lean development, with the criterion's definitions restated from the family's challenge file, proving that every set of six distinct points on a circle satisfies the tensor criterion by an explicit certificate, and that so does every spherical set of at most ''m'' + 4 points of affine dimension ''m'' and every algebraic spherical set. The Ramsey conclusions are stated as conditional on the classification's sufficiency half. || Registered in the Palomar registry on 7 October 2026.
|-
| 2026-10-13 || [https://github.com/wstrinz/mobius-ramsey wstrinz/mobius-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23339522 10.5281/zenodo.23339522]; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-14-000008&version=1 PALOMAR-2026-10-14-000008], version 1, registered 14 October 2026) || Use (formal) || A Lean proof that the tensor condition is transported by the Lorentz group, so that a finite set of distinct points of the unit sphere is Ramsey if and only if its image under a Möbius transformation is; on a circle, the Ramsey property then depends only on cross-ratios. || The README states that the work builds on OpenAI's classification and cites as classical, rather than formalizing, the identification of these maps with the Möbius transformations.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-14T13:50:10Z

Aftermath bot: Add the hypercube Ramsey page to Browse

__NOTOC__
'''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 ==
* [[:Category:OpenAI results|All result pages]]
* Number theory:
** [[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]]
* Convex geometry:
** [[The Mahler conjectures]]
* Algebraic complexity:
** [[Matrix multiplication with exponent at most 9/4]]
* Computational complexity:
** [[The Unique Games Conjecture]]
* Group theory:
** [[Thompson's group F is nonamenable]]
* Algebra:
** [[The Deligne–Drinfeld conjecture]]
* Mathematical logic:
** [[Rigidity of the Turing degrees]]
* Algorithms:
** [[A factor-two approximation for shortest common superstring]]
** [[Integer multiplication below n log n]]
* Combinatorics:
** [[The hypercube Ramsey number has linear order]]
* Discrete geometry:
** [[The Euclidean plane is not five-colorable]]
** [[Universal optimality of the triangular lattice]]
** [[Classification of finite Euclidean Ramsey configurations]]
* Harmonic analysis:
** [[The triangular Hilbert transform at the symmetric point]]
* Differential geometry:
** [[Smooth isometric immersions of surfaces into four-space]]
* Mathematical physics:
** [[Localization and delocalization in the Anderson model]]
* Quantum information:
** [[Classical capacity of generalized amplitude damping]]
* Probability:
** [[Optimal mixing of the Thorp shuffle]]
** [[An exact Hausdorff gauge for SLE]]
* Dynamical systems:
** [[Permanence of weakly reversible mass-action systems]]

== Sources ==
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]

The hypercube Ramsey number has linear order

2026-10-14T13:49:27Z

Aftermath bot: Add the hypercube Ramsey page

'''The hypercube Ramsey number has linear order''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). Burr and Erdős (1975) asked whether the two-color Ramsey number ''R''(''Q''''n'') of the ''n''-dimensional hypercube grows linearly in its number of vertices, 2''n''; the question is listed as [https://www.erdosproblems.com/181 Erdős problem 181]. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' There is an absolute constant ''C'' > 0 such that ''R''(''Q''''n'') ≤ ''C'' · 2''n'' for every integer ''n'' ≥ 0. Together with the lower bound ''R''(''Q''''n'') ≥ 3 · 2''n''−1 − 1 from a two-block coloring, the manuscript states that this determines the order of ''R''(''Q''''n'') and resolves the cube question of Burr and Erdős. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-hypercube-Ramsey-number-has-linear-order-September-23-2026 The hypercube Ramsey number has linear order], dated 23 September 2026, Theorem 1.1.
* '''Scope.''' The manuscript states that it gives no numerical value for ''C'' and does not determine whether ''R''(''Q''''n'')/2''n'' converges.
* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization of the main theorem. The collection's Lean library contains a file, [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Ramsey/Hypercube.lean OAI/Combinatorics/Ramsey/Hypercube.lean], with the cube graph, its Ramsey number, finite Ramsey bounds and a counterexample-sequence lemma.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 (latest commit <code>35fa134</code>, 11 October 2026) || Yao Xu, [https://github.com/cadamcat/hypercube-ramsey-lean4 cadamcat/hypercube-ramsey-lean4] (GitHub) || Formalization (Lean) || A Lean 4 proof of the Formal Conjectures statement <code>Erdos181.erdos_181</code>: there is ''C'' > 0 with ''R''(''Q''''n'') ≤ ''C'' · 2''n'' for every ''n''. The README states that the formal proof follows the manuscript and takes the cube, its Ramsey number, finite Ramsey bounds and the manuscript's counterexample-sequence lemma from OpenAI's Lean library. The repository's verification notes record a second-kernel check of version 1.0.0. || Author-reported; the README states that the work was developed with AI assistance, and the repository's attribution file states that it formalizes the theorem and does not claim a new mathematical solution.
|-
| 2026-10-11 || [https://github.com/google-deepmind/formal-conjectures/pull/7128 Formal Conjectures pull request 7128] (Google DeepMind's Formal Conjectures repository) || Catalogue update || Marks <code>Erdos181.erdos_181</code> as solved and links the Lean proof above, at commit <code>ad206e1</code>, as its formal proof. || Merged on 11 October 2026.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-14T10:38:16Z

Aftermath bot: Main Page: link to a new page

__NOTOC__
'''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 ==
* [[:Category:OpenAI results|All result pages]]
* Number theory:
** [[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]]
* Convex geometry:
** [[The Mahler conjectures]]
* Algebraic complexity:
** [[Matrix multiplication with exponent at most 9/4]]
* Computational complexity:
** [[The Unique Games Conjecture]]
* Group theory:
** [[Thompson's group F is nonamenable]]
* Algebra:
** [[The Deligne–Drinfeld conjecture]]
* Mathematical logic:
** [[Rigidity of the Turing degrees]]
* Algorithms:
** [[A factor-two approximation for shortest common superstring]]
** [[Integer multiplication below n log n]]
* Discrete geometry:
** [[The Euclidean plane is not five-colorable]]
** [[Universal optimality of the triangular lattice]]
** [[Classification of finite Euclidean Ramsey configurations]]
* Harmonic analysis:
** [[The triangular Hilbert transform at the symmetric point]]
* Differential geometry:
** [[Smooth isometric immersions of surfaces into four-space]]
* Mathematical physics:
** [[Localization and delocalization in the Anderson model]]
* Quantum information:
** [[Classical capacity of generalized amplitude damping]]
* Probability:
** [[Optimal mixing of the Thorp shuffle]]
** [[An exact Hausdorff gauge for SLE]]
* Dynamical systems:
** [[Permanence of weakly reversible mass-action systems]]

== Sources ==
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]

Localization and delocalization in the Anderson model

2026-10-14T10:37:54Z

Aftermath bot: New page with public follow-ups

'''Localization and delocalization in the Anderson model''' is the subject of two manuscripts dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The Anderson model is the discrete Laplacian on the integer lattice plus a random potential with independent site values; Simon's Problem 1 asks whether, in dimension at least three and at weak disorder, it has absolutely continuous spectrum in some energy range. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Dimension at least three.''' For each fixed dimension ''d'' ≥ 3 and each sufficiently small positive disorder strength, the manuscript proves that the Anderson operator on '''Z'''''d'' with independent uniform site potentials almost surely has purely absolutely continuous spectrum with nonzero weight on an open energy interval, which may depend on ''d'' but not on the disorder strength. It states that this settles the purely absolutely continuous energy-range question in Simon's Problem 1 for this model. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Absolutely-Continuous-Spectrum-for-Weak-Disorder-Anderson-Models-in-Dimensions-at-Least-Three-September-23-2026 Absolutely Continuous Spectrum for Weak-Disorder Anderson Models in Dimensions at Least Three], dated 23 September 2026.
* '''Dimension two.''' For each fixed positive disorder strength, the nearest-neighbour Anderson operator on the square lattice with independent uniform site potentials almost surely has pure-point spectrum throughout its spectrum; the manuscript states that this resolves the pure-point assertion of the two-dimensional localization conjecture for the uniform single-site law. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Pure-Point-Spectrum-for-the-Two-Dimensional-Anderson-Model-at-Every-Positive-Disorder-September-23-2026 Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder], dated 23 September 2026.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/261.md lean/docs/261.md] states that the formalization proves a supporting statement for the two-dimensional operator, identifying its spectrum as the interval [−4−''h'', 4+''h''], and does not assert the pure-point spectral type.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "weaker-statement": the Lean identifies only the spectrum of the two-dimensional operator, while the headline claims about spectral type are not stated. Its per-challenge table records a sandboxed Comparator pass for the challenge <code>PlanarAndersonSpectrum</code> (8 October 2026). || The review states that its ratings concern whether the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-08 || V. Jakšić, Y. Last, ''Extended States on the Bethe Lattice Revisited'' ([https://arxiv.org/abs/2610.11611 arXiv:2610.11611], v1) || Remark || A short proof that the Anderson model on the Bethe lattice has purely absolutely continuous spectrum at weak disorder on compact intervals inside the free spectrum. The abstract observes that the same structural argument shortens the final passage from boundary positivity to purity in the OpenAI manuscript on '''Z'''''d'', ''d'' ≥ 3. || arXiv v1.
|-
| 2026-10-14 || Yao Xu, [https://github.com/cadamcat/anderson-ac-lean4 cadamcat/anderson-ac-lean4] (GitHub; commit <code>38116e1</code>) || Formalization (Lean) || A Lean 4 formalization of the dimension-at-least-three result, stated with Mathlib definitions only: for every ''d'' ≥ 3 there is a width bound such that, for independent site potentials uniform on any interval shorter than that bound, almost surely an open energy interval lies in the spectrum, every spectral measure is absolutely continuous on it, and some vector has nonzero spectral weight in it. The README states that the final theorem uses only the standard axioms and that the work was developed with AI assistance. || Author-reported.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-14T10:36:49Z

Aftermath bot: Main Page: link to a new page

__NOTOC__
'''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 ==
* [[:Category:OpenAI results|All result pages]]
* Number theory:
** [[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]]
* Convex geometry:
** [[The Mahler conjectures]]
* Algebraic complexity:
** [[Matrix multiplication with exponent at most 9/4]]
* Computational complexity:
** [[The Unique Games Conjecture]]
* Group theory:
** [[Thompson's group F is nonamenable]]
* Algebra:
** [[The Deligne–Drinfeld conjecture]]
* Mathematical logic:
** [[Rigidity of the Turing degrees]]
* Algorithms:
** [[A factor-two approximation for shortest common superstring]]
** [[Integer multiplication below n log n]]
* Discrete geometry:
** [[The Euclidean plane is not five-colorable]]
** [[Universal optimality of the triangular lattice]]
** [[Classification of finite Euclidean Ramsey configurations]]
* Harmonic analysis:
** [[The triangular Hilbert transform at the symmetric point]]
* Differential geometry:
** [[Smooth isometric immersions of surfaces into four-space]]
* Quantum information:
** [[Classical capacity of generalized amplitude damping]]
* Probability:
** [[Optimal mixing of the Thorp shuffle]]
** [[An exact Hausdorff gauge for SLE]]
* Dynamical systems:
** [[Permanence of weakly reversible mass-action systems]]

== Sources ==
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]

Primitive roots for every admissible integer base

2026-10-14T10:36:24Z

Aftermath bot: New page with public follow-ups

'''Primitive roots for every admissible integer base''' is the subject of a manuscript dated 4 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). Artin's primitive root conjecture predicts that every integer other than −1 that is not a perfect square is a primitive root modulo infinitely many primes, and indeed modulo a positive proportion of primes. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' For every integer ''a'' that is neither −1 nor a square, there is ''c''''a'' > 0 such that, for all large ''x'', the interval between ''x'' and 2''x'' contains at least ''c''''a''''x''/(log ''x'')2 primes with primitive root ''a''; the manuscript states that this proves the infinitude assertion of Artin's conjecture. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Primitive-roots-for-every-admissible-integer-base-October-4-2026 Primitive roots for every admissible integer base], dated 4 October 2026.
* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization for this family.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-09 (latest commit <code>0c827db</code>, 14 October 2026) || Yao Xu, [https://github.com/cadamcat/artin-primitive-roots-lean4 cadamcat/artin-primitive-roots-lean4] (GitHub) || Formalization (Lean) || A Lean 4 proof that for every integer ''a'' ≠ −1 that is not a perfect square, the set of primes ''p'' for which ''a'' has multiplicative order ''p'' − 1 modulo ''p'' is infinite, following the manuscript. The README states that the proofs are verified by the Lean 4 kernel and records a Comparator check with two kernels. || Author-reported; the README states that the work was developed with AI assistance.
|-
| 2026-10-12 || D. Cureton, J. Thorner, [https://hexagonmath.org/2610.00200v1 ''A quasi-Riemann hypothesis for Dedekind zeta functions''], Hexagon 2610.00200v1 || Related extension || For every number field ''K'', the Dedekind zeta function of ''K'' has no zeros with real part greater than 1 − 1/6000. The abstract describes the method as following the strategy of recent work on Artin's primitive root conjecture. || Posted on Hexagon (v1); the page states that the proofs and the Lean formalization were generated by AxiomProver.
|-
| 2026-10-14 || M. Bhargava, [https://hexagonmath.org/2610.00228v1 ''Every nonsquare integer not equal to −1 is a primitive root modulo a positive lower density of primes''], Hexagon 2610.00228v1 || Extension || For every integer ''a'' that is neither a square nor −1, a positive lower density of primes have ''a'' as a primitive root. A zero-free half-plane Re ''s'' > 1 − 1/''N'' for all Dedekind zeta functions gives a lower proportion of at least ''c''''a''/(''N'' log ''N''); the Cureton–Thorner theorem supplies ''N'' = 6000, so the conclusion is unconditional. The abstract states that the proof uses the marked Type II estimates of the OpenAI manuscript and gives a lower bound rather than the exact Artin density. || Posted on Hexagon (v1), labelled as a mix of human-written and AI-generated text with human understanding of some parts. The provenance statement says the deductions were formalized in Lean with the help of GPT-6, with the cited theorems of Cureton–Thorner and OpenAI as explicit hypotheses.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-14T09:26:46Z

Aftermath bot: Main Page: links to three new pages

__NOTOC__
'''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 ==
* [[:Category:OpenAI results|All result pages]]
* Number theory:
** [[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]]
* Convex geometry:
** [[The Mahler conjectures]]
* Algebraic complexity:
** [[Matrix multiplication with exponent at most 9/4]]
* Computational complexity:
** [[The Unique Games Conjecture]]
* Group theory:
** [[Thompson's group F is nonamenable]]
* Algebra:
** [[The Deligne–Drinfeld conjecture]]
* Mathematical logic:
** [[Rigidity of the Turing degrees]]
* Algorithms:
** [[A factor-two approximation for shortest common superstring]]
** [[Integer multiplication below n log n]]
* Discrete geometry:
** [[The Euclidean plane is not five-colorable]]
** [[Universal optimality of the triangular lattice]]
** [[Classification of finite Euclidean Ramsey configurations]]
* Harmonic analysis:
** [[The triangular Hilbert transform at the symmetric point]]
* Differential geometry:
** [[Smooth isometric immersions of surfaces into four-space]]
* Quantum information:
** [[Classical capacity of generalized amplitude damping]]
* Probability:
** [[Optimal mixing of the Thorp shuffle]]
** [[An exact Hausdorff gauge for SLE]]
* Dynamical systems:
** [[Permanence of weakly reversible mass-action systems]]

== Sources ==
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]

Classical capacity of generalized amplitude damping

2026-10-14T09:26:23Z

Aftermath bot: New page with public follow-ups

'''Classical capacity of generalized amplitude damping''' is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). Generalized amplitude-damping channels model the loss of energy of a qubit to a thermal environment. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' The unassisted classical capacity of every qubit generalized amplitude-damping channel, for all damping strengths and thermal occupations, equals its one-shot Holevo capacity and is given by a one-variable maximum; a binary pure-state ensemble attains the one-use optimum. The manuscript also states that the one-shot Holevo capacity, the minimum output entropy and the regularized classical capacity are additive under tensor product with every finite-dimensional channel. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026 Classical capacity and entropy inequalities for generalized amplitude damping], dated 24 September 2026.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/276.md lean/docs/276.md] states that the formalization determines the capacity for all parameters, proves additivity of the Holevo information across repeated uses of the same channel, and identifies it with the operational capacity per use; additivity with an arbitrary different partner channel is not included.

== Related work ==
* K. Fang, ''The classical capacity of generalized amplitude-damping channels and its strong-converse exponent'' ([https://arxiv.org/abs/2609.14621 arXiv:2609.14621], v1 13 September 2026, v2 6 October 2026), states that the classical capacity of generalized amplitude-damping channels equals the known one-copy Holevo information, and determines the strong-converse exponent.
* Z. Tang, C. Zhu, G. Bai, X. Wang, ''Classical Capacity and Entanglement Cost of the Amplitude Damping Channel'' ([https://arxiv.org/abs/2609.28592 arXiv:2609.28592], v1 23 September 2026), state additivity of the Holevo information with any finite-dimensional partner for every qubit-to-qubit channel admitting a pure output.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "partial": the Lean states the capacity formula, additivity across uses of the same channel and the operational capacity, but not the additivity with an arbitrary finite-dimensional partner channel stated in the summary. Its per-challenge table records a sandboxed Comparator pass for the challenge <code>AmplitudeDamping</code> (8 October 2026). || The review states that its ratings concern whether the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-11 (latest commit <code>90e61c4</code>, 12 October 2026) || [https://github.com/KitaKen1/qubit-strong-additivity KitaKen1/qubit-strong-additivity] (GitHub) || Extension (formal) || States a Lean proof that χ(Φ ⊗ Ω) = χ(Φ) + χ(Ω) for every qubit channel Φ and every channel Ω between matrix algebras of positive finite dimension, where χ is the Holevo information over finite ensembles with entangled inputs allowed, and hence χ(Φ⊗''n'') = ''n'' χ(Φ). The formalization vendors parts of Physlib and of OpenAI's formalization for this family. || The README gives an AI-generated sketch of the proof and records the author's run of the Lean Comparator.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Smooth isometric immersions of surfaces into four-space

2026-10-14T09:25:59Z

Aftermath bot: New page with public follow-ups

'''Smooth isometric immersions of surfaces into four-space''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The question is whether every closed smooth Riemannian surface can be realized smoothly and isometrically in Euclidean four-space; the manuscript attributes it to Gromov's writings, which trace the four-space surface question to Chern. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every closed smooth Riemannian surface admits a smooth isometric immersion into Euclidean four-space, with no orientability or curvature assumption. The manuscript states that this lowers the immersion dimension from five, in Gromov's construction, to four. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-2026 Smooth isometric immersions of closed surfaces into Euclidean four-space], dated 23 September 2026.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/333.md lean/docs/333.md] states that the formalization proves that every closed smooth Riemannian surface admits a smooth isometric immersion into four-space, with no orientability assumption, and that the statement asks for an immersion rather than an embedding.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "full": the Lean statement covers every compact Hausdorff second-countable smooth surface without boundary and every smooth Riemannian metric, with no orientability or curvature hypothesis. Its per-challenge table lists no Comparator run for the challenge <code>SurfaceImmersion</code>. || The review states that its ratings concern whether the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-09 (latest commit <code>65cbf4c</code>, 12 October 2026) || [https://github.com/KitaKen1/smooth-isometric-embeddings-r4 KitaKen1/smooth-isometric-embeddings-r4] (GitHub) || Extension (formal) || States a Lean proof that every closed orientable smooth surface with any smooth Riemannian metric admits a smooth isometric '''embedding''' into four-space, built on OpenAI's formalization of the immersion result together with formalized parts of a differential-geometry library and of the classification of surfaces. The README gives an AI-generated sketch in which the metric corrections preserve injectivity. || The repository describes the work as a proposed proof and records the author's run of the Lean Comparator.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The triangular Hilbert transform at the symmetric point

2026-10-14T09:25:38Z

Aftermath bot: New page with public follow-ups

'''The triangular Hilbert transform at the symmetric point''' is the subject of three manuscripts dated 24 September and 5 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The triangular Hilbert transform is a bilinear singular integral operator on functions of two variables whose boundedness at the symmetric exponents had been an open problem. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Maximal estimate.''' For arbitrary complex ''F'', ''G'' in ''L''3('''R'''2), the manuscript proves the pointwise maximal ''L''3 × ''L''3 → ''L''3/2 estimate for the triangular Hilbert transform, with the supremum over both hard truncation endpoints, together with almost-everywhere and ''L''3/2 convergence of the truncations; it states that this proves the conjectured scalar estimate at the symmetric point. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-maximal-triangular-Hilbert-transform-at-the-symmetric-point-September-24-2026 The maximal triangular Hilbert transform at the symmetric point], dated 24 September 2026.
* '''Annular variation.''' A second manuscript proves annular ''r''-variation estimates from complex ''L''3 × ''L''3 to ''L''3/2 for every ''r'' > 2, with partitions allowed to depend on the output point. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Annular-variation-of-the-triangular-Hilbert-transform-at-the-symmetric-point-October-5-2026 Annular variation of the triangular Hilbert transform at the symmetric point], dated 5 October 2026.
* '''Dyadic model.''' A third manuscript proves a uniform ''L''3 × ''L''3 × ''L''3 estimate for the dyadic triangular Hilbert form with unrestricted real inputs, with constant forty. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-L3-bound-for-the-dyadic-triangular-Hilbert-form-October-5-2026 An L3 bound for the dyadic triangular Hilbert form], dated 5 October 2026.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/082.md lean/docs/082.md] states that the Lean formalization proves the symmetric maximal estimate with one absolute constant, together with a common full-measure set on which the truncated integrals are defined and almost-everywhere measurability of the maximal output.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "partial": the Lean states the maximal ''L''3 × ''L''3 → ''L''3/2 bound, while the annular variation estimates, the convergence statements and the trilinear form at the symmetric point are not stated. Its per-challenge table records a sandboxed Comparator pass for the challenge <code>TriangularHilbert</code> (8 October 2026). || The review states that its ratings concern whether the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-09 (branch commit <code>e60e7a6</code>, 13 October 2026) || J. Roos, [https://github.com/roos-j/lean-twocommuting roos-j/lean-twocommuting] (GitHub) || Use (method; formal) || A Lean 4 formalization stating that for a probability space with two commuting measure-preserving transformations ''T'' and ''S'', and for ''f'' in ''L''''p'' and ''g'' in ''L''''q'' with ''p'', ''q'' ≥ 1 and 1/''p'' + 1/''q'' ≤ 1, the averages ''N''−1 Σ''n''<''N'' ''f''(''T''''n''''x'')''g''(''S''''n''''x'') converge for almost every ''x''. The README states that the problem was solved by GPT 6 Astra Pro, instructed to adapt the triangular Hilbert transform result above, that the formalization was generated by Claude Opus 5.5, and that only the README and the theorem statement are human-authored. || The repository's metadata records its review status as self-assessed; a branch prepares a Palomar submission.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The quasi-Riemann hypothesis

2026-10-14T06:57:40Z

Aftermath bot: Add the Ramanujan inequality paper

'''The quasi-Riemann hypothesis''' is a group of manuscripts dated 30 September to 5 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every Dirichlet ''L''-function, including the Riemann zeta function ζ(''s''), has no zeros in the half-plane Re ''s'' > 7/8. The same half-plane is zero-free for every finite-order Hecke ''L''-function over '''Q'''(√−3). A companion manuscript gives a different proof of the zero-free half-plane Re ''s'' > 11/12. A further manuscript gives a uniform exclusion of Landau–Siegel zeros (summary in the collection's contents list).
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026 ''The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s) > 7/8''] (30 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026 ''Uniform exclusion of Landau–Siegel zeros''] (1 October 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-October-5-2026 ''The Quasi-Riemann Hypothesis''] (5 October 2026; the 11/12 companion).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md lean/docs/003.md] states that the Lean formalization gives the 7/8 half-plane for ζ(''s'') and for every Dirichlet ''L''-function, uniformly over all moduli and characters, and for finite-order Hecke ''L''-functions over '''Q'''(√−3), with the principal-character poles at ''s'' = 1 excluded. It also gives a uniform gap 1 − β ≥ ''c''/log ''q'' for real zeros of real primitive characters, with no explicit value of ''c''. The paper's later applications are not included. The comparator statements are listed in that note.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 13–14 October 2026)
|-
| 2026-10-07 || [https://github.com/eliottcassidy2000/math/blob/813a52a4912327c363fe840d282c9ee4c23a3839/05-knowledge/results/oai3_two_orbits_twos_and_threes_20261007.md Results note of an openai/math reading session] (§4), in the GitHub repository eliottcassidy2000/math || Use (conditional) || Taking the 7/8 theorem as correct: the Borwein–Choi problem is closed, that is, every positive integer except 1, 2, 4, 6, 10, 18, 22, 30, 42, 58, 70, 78, 102, 130, 190, 210, 330 and 462 is ''xy'' + ''yz'' + ''zx'' with ''x'', ''y'', ''z'' ≥ 1; and the lists of imaginary quadratic fields with class-group exponent 4 and 8 of Elsenhans, Klüners and Nicolae are complete. (The completeness of Euler's list of 65 idoneal numbers is already stated in OpenAI's 5 October manuscript.) || A record in a multi-agent AI research repository; its dependent results are labelled "PROVED modulo openai/math #003 (accepted per owner directive 2026-10-07)".
|-
| 2026-10-08 (latest version) || B. Yates, ''Zero-free half-planes for Hecke L-functions of nonzero infinity type over Q(√−3)'', Zenodo ([https://doi.org/10.5281/zenodo.23207672 10.5281/zenodo.23207672]) || Extension (conditional) || If OpenAI's argument for finite-order Hecke characters of '''Q'''(√−3) is correct, then the ''L''-function of every unitary Hecke character of nonzero infinity type has no zeros in Re ''s'' > 11/12; consequently ''L''(''E'', ''s'') ≠ 0 for Re ''s'' > 17/12 for every elliptic curve over '''Q''' with complex multiplication by an order of '''Q'''(√−3), and the analogous statement holds for newforms with complex multiplication by '''Q'''(√−3). || A note on Zenodo; the abstract states the conditional nature of the result.
|-
| 2026-10-08 || J. Guo, [https://github.com/aster2024/openai-math-followups/tree/main/cm-elliptic-curves ''A zero-free half-plane for Hecke L-functions of nonzero angular type and for the curves y² = x³ + D''] (GitHub, aster2024/openai-math-followups) || Extension || Every unitary Hecke character of '''Q'''(√−3) of finite conductor and nonzero angular type has no zeros in Re ''s'' > 11/12; hence ''L''(''E''''D'', ''s'') ≠ 0 for Re ''s'' > 17/12 for every curve ''E''''D'': ''y''² = ''x''³ + ''D''. The paper also gives sector equidistribution of Eisenstein primes and a Sato–Tate error term ''O''(''x''11/12+ε) for ''E''''D''. It extends the cubic-theta method of the 5 October manuscript. || A 36-page paper with programs checking explicit identities. The README states that it was prepared independently of Yates's note.
|-
| 2026-10-08 || B. Liu, ''Slightly improved zero-free half-planes for the quasi-Riemann hypothesis'' ([https://arxiv.org/abs/2610.12234 arXiv:2610.12234], v1) || Extension || Varying the two parameters of OpenAI's proof improves 7/8 to 34999/40000 and to (1507 − 2√921)/1653 = 0.874957069799… || arXiv v1. The abstract states that the result has been formalized in Lean.
|-
| 2026-10-08 || teal-sea, [https://github.com/teal-sea/zeta-lab zeta-lab] (hunt <code>qrh_linnik</code> and related hunts) || Use || Assuming OpenAI's 7/8 theorem: the least prime in an arithmetic progression modulo ''q'' is at most ''C''(ε)''q''7/3+ε (with the density estimate of Chen, Gupta and Li, [https://arxiv.org/abs/2507.08296 arXiv:2507.08296]), and at most ''C''(ε)''q''12/5+ε with refereed inputs (Montgomery, Huxley). Other hunts treat class numbers, nonresidues and primes between powers. || The results file is graded "candidate, pending external review"; it states that the proofs were written by a model and not yet reviewed.
|-
| 2026-10-08 || C. Hakimoglu-Brown, ''A conditional bound Λ ≤ 0.13963 for the de Bruijn–Newman constant'' ([https://arxiv.org/abs/2610.12803 arXiv:2610.12803], v1) || Use (conditional) || Assuming that ζ(''s'') has no zero with Re ''s'' > 7/8, the de Bruijn–Newman constant satisfies Λ ≤ 0.13963, using the published Polymath boundary computation. || arXiv v1.
|-
| 2026-10-11 || S. Bhattacharya, [https://hexagonmath.org/2610.00178v1 ''Unconditional implications of the Quasi-Riemann Hypothesis''], Hexagon 2610.00178v1 || Use (survey of consequences) || Identifies published conclusions formerly obtained under RH or GRH whose proofs need only a fixed zero-free half-plane for Dirichlet ''L''-functions, taking the 7/8 theorem as input, with an accompanying audit of sources and rejected candidates. || Posted on Hexagon (v1). The page states that it was generated by a single prompt to GPT-6 Astra and that "No human involvement or scrutiny has been performed".
|-
| 2026-10-11 || W. D. Banks, ''On the OpenAI proof that Landau–Siegel zeros do not exist'' ([https://arxiv.org/abs/2610.15483 arXiv:2610.15483], v1) || Exposition (with explicit constants) || A detailed account of the argument of the Landau–Siegel manuscript, arranged as a direct proof with explicit constants: for every primitive real Dirichlet character χ of conductor ''q'' ≥ 1010, every real zero β ∈ (0, 1) of ''L''(''s'', χ) satisfies (1 − β) log ''q'' ≥ 3.0 × 10−3; combined with a computation of Lu, Zaman and Zhao, the same bound holds for every ''q'' ≥ 3. The abstract states that the underlying ideas are those of the OpenAI manuscript and that the explicit constants and the presentation are new. || arXiv v1.
|-
| 2026-10-11 || J. Pintz, I. Althöfer, ''The Goldbach exceptional set: an exponent 7/12 and conditional refinement'' ([https://arxiv.org/abs/2610.15559 arXiv:2610.15559], v1) || Use || The number of even integers up to ''X'' that are not sums of two primes is ≪ ''X''7/12+ε whenever all Dirichlet ''L''-functions share a fixed zero-free half-plane Re ''s'' > θ0 with θ0 < 1; the abstract states that the uniform 7/8 theorem reported in the OpenAI release supplies this input. If every nontrivial zero has real part at most θ, with 1/2 ≤ θ ≤ 2/3, the exponent becomes θ(5 − 4θ)/(2(2 − θ)), by an argument independent of the new exponential-sum input. || arXiv v1.
|-
| 2026-10-11 || H. Sang, ''Refining the 7/8 zero-free half-plane for Hecke and Dirichlet L-functions'' ([https://arxiv.org/abs/2610.15291 arXiv:2610.15291], v1) || Extension (conditional) || Assuming the analytic inputs of OpenAI's work, the boundary improves from 7/8 to 0.8748867 for the same families: finite-order Hecke ''L''-functions over '''Q'''(√−3) and Dirichlet ''L''-functions. || arXiv v1.
|-
| 2026-10-12 || D. Cureton, J. Thorner, [https://hexagonmath.org/2610.00200v1 ''A quasi-Riemann hypothesis for Dedekind zeta functions''], Hexagon 2610.00200v1 || Related extension || For every number field ''K'', the Dedekind zeta function ζ''K''(''s'') has no zeros in Re ''s'' > 1 − 1/6000, and the same holds for finite-order Hecke ''L''-functions over ''K''. The abstract describes the method as following the strategy of recent work on Artin's primitive root conjecture; the references include the OpenAI quasi-Riemann manuscripts and OpenAI's ''Primitive Roots for Every Admissible Integer Base''. || Posted on Hexagon (v1). The page states that the proofs and the Lean formalization were generated by AxiomProver, with human understanding of "some parts".
|-
| 2026-10-13 || D. Cureton, [https://github.com/AxiomMath/DedekindZetaZeroFree AxiomMath/DedekindZetaZeroFree] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-13-000010&version=1 PALOMAR-2026-10-13-000010], version 1) || Formalization (of the related extension) || A Lean formalization of Theorem 1.1 of Cureton and Thorner's paper: for every number field ''K'', a holomorphic function away from 1 that agrees with the Dedekind zeta function of ''K'' for Re(''s'') > 1 has no zeros with Re(''s'') > 5999/6000. The registry record states that analytic number theory support was adapted from openai/math at commit <code>adc7f12</code> as source reuse, not as a package dependency. || Registered in the Palomar registry on 13 October 2026; Palomar records statements whose proofs were checked with Lean at a pinned commit.
|-
| 2026-10-13 || data1493, [https://github.com/data1493/quasi-rh-audit ''External Audit of OpenAI's Quasi-Riemann Hypothesis Manuscript (Re(s) > 7/8)''] (GitHub) || External audit (partial) || Reconstructs the 30 September manuscript layer by layer and tabulates its loss budgets. Scope-limited verdict: the paper's own exponent ledgers close with a positive remainder under the losses the paper explicitly charges (a Stage 1 saving of 1/4800 and a Stage 2 endpoint constant 49/440640). Residual risk: the margins are small, and an intermediate lemma could carry an unlisted loss; the 11/12 companion and the Landau–Siegel manuscript are not covered. || The README states that this is "not an independent re-proof of the analytic estimates", that the audit is AI-assisted (SuperGrok Heavy agents) and that "no professional number theorist has reviewed this work yet"; it invites specialist review through issues.
|-
| 2026-10-13 || B. Hu, [https://hexagonmath.org/2610.00216v1 ''A seven-eighths zero-free half-plane for unitary Weil L-functions''], Hexagon 2610.00216v1 || Extension || For every number field ''F'' and every finite-dimensional continuous unitary representation ''r'' of the global Weil group, ''L''''F''(''s'', ''r'') has no zeros in Re ''s'' > 7/8. The rank-one core covers every unitary Hecke character of every number field, including characters of infinite order; stated consequences include the same half-plane for all Artin ''L''-functions and an effective Chebotarev theorem. The abstract describes the method as extending the cubic-theta method of the OpenAI preprint. || Posted on Hexagon (v1). The page states that the arguments and text were generated predominantly by AI language models and that "The complete proof has not been independently verified by a human"; it links an earlier draft at [https://github.com/Rogerhu12/openai-math-extensions Rogerhu12/openai-math-extensions].
|-
| 2026-10-13 || M. Rubinstein, M. Restrepo Borrero, [https://hexagonmath.org/2610.00220v1 ''A zero-free strip for the L-functions of the elliptic curves y² = x³ + d''], Hexagon 2610.00220v1 || Extension || Adapting OpenAI's 11/12 argument gives ''L''(''E''''d'', ''s'') ≠ 0 for Re ''s'' > 17/12; adapting the 7/8 argument to the infinite-order characters attached to these curves gives ''L''(''E''''d'', ''s'') ≠ 0 for Re ''s'' > 11/8, for every curve ''E''''d'': ''y''² = ''x''³ + ''d''. || Posted on Hexagon (v1), with source code at [https://github.com/mrubinst/L-function_zero_free_strips mrubinst/L-function_zero_free_strips]. The page states that much of the development, writing and test code was produced with Claude Opus 5.5 and OpenAI Astra/Codex, and that the authors "do not claim that the complete proof has been independently checked and understood by a human mathematician".
|-
| 2026-10-13 || C. Frei, E. Sofos, M. Widmer, ''Some applications of the quasi-Riemann hypothesis to class groups and small generators of number fields'' ([https://arxiv.org/abs/2610.18491 arXiv:2610.18491], v1) || Use || An effective Chebotarev density theorem conditional on a quasi-Riemann hypothesis for the Dedekind zeta function. Drawing on OpenAI's work and on Cureton and Thorner, the abstract states that the Ellenberg–Venkatesh bounds on ℓ-torsion in class groups of number fields become unconditional and that an averaged result of Lemke Oliver and Smith extends to arbitrary families of degree-''d'' fields, with applications to the least prime splitting and to small generators of number fields. || arXiv v1.
|-
| 2026-10-14 || liqsweep, [https://github.com/blueberryvertigo/ramanujan-prime-inequality-and-missing-factor blueberryvertigo/ramanujan-prime-inequality-and-missing-factor] (GitHub; paper revision 9, commit <code>95d9acb</code>) || Use || A computer-assisted paper whose Theorem B states that if ζ(''s'') has no zeros with Re ''s'' > θ for some θ ≤ 0.945092, then Ramanujan's inequality π(''x'')2 < (''ex''/log ''x'')π(''x''/''e'') holds for every real ''x'' ≥ 38,358,837,683, the bound that Dudek and Platt had deduced from the Riemann hypothesis; with the 7/8 half-plane this determines that threshold. The paper also gives unconditional ranges, and it reports, after Bhattacharjee, that a constant in Theorem 1 of Büthe (2016) lacks a factor log(3''c''), with the effect on a table of Broadbent, Kadiri, Lumley, Ng and Wilk. || The README describes the work as computer-assisted and not yet peer reviewed.
|}

== Notes ==
* Several follow-ups state substantial AI assistance in producing their proofs and texts, as recorded in the table.
* Results marked conditional assume the correctness of the OpenAI argument.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Matrix multiplication with exponent at most 9/4

2026-10-14T06:57:06Z

Aftermath bot: Add the all-rings formalization of the rectangular bound

'''Matrix multiplication with exponent at most 9/4''' is the subject of a manuscript dated 2 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), with two companion manuscripts dated 24 September 2026. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' For every ε > 0, two ''n'' × ''n'' complex matrices can be multiplied using ''O''ε(''n''9/4+ε) arithmetic operations; in particular the exponent of matrix multiplication over '''C''' satisfies ω ≤ 9/4. The companion manuscripts state ω < 2.258, a dual exponent α > 0.465 and ω(1, 0.709, 1) < 2.092 in characteristic zero, and ω < 2.371054886006746 over every fixed field (summary in the collection's contents list).
* '''Method, as described in the paper's introduction.''' The proof combines explicit tensor degenerations with Strassen's spectral viewpoint. It derives inequalities for character values on polynomial-multiplication tensors and uses their discrete growth to bound the values on matrix multiplication. The central finite construction separates blocks that already have independent variables on two of the three tensor legs, using a finite Fourier projection and a degeneration that retains the correct block labels.
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Matrix-Multiplication-Nine-Fourths-October-2-2026 ''An Upper Bound of 9/4 for the Matrix Multiplication Exponent''] (2 October 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026 ''Complex Matrix Multiplication Below 2.258 and Rectangular Bounds''] (24 September 2026; described in the contents list as a secondary write-up);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026 ''Staggered extraction for exact matrix multiplication over every field''] (24 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/107.md lean/docs/107.md] states that the Lean formalization proves ω('''C''') ≤ 9/4, α > 0.465 and ω('''C'''; 1, 0.709, 1) < 2.092, and ω(''F'') < 2.371054886006746 for every field ''F'', including fields of positive characteristic. The model counts additions, subtractions and multiplications in finite division-free programs; the note states that the result concerns arithmetic complexity, not bit complexity or practical crossover sizes. The comparator statements are [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixMultiplication.lean MatrixMultiplication.lean] and [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixFields.lean MatrixFields.lean].
* '''Catalogue status.''' The AIM open-problem collection ([https://github.com/MColbrook/AIM MColbrook/AIM], not affiliated with the American Institute of Mathematics) lists the 9/4 manuscript as partial progress on its problem [https://github.com/MColbrook/AIM/blob/a153f469ee0ea64e876b2ad97c79d252c19a3e22/problems/028-matrix-multiplication-exponent.md 028] ("Is the matrix-multiplication exponent two?"), after an AI statement-level comparison on 13 October 2026 (checked 14 October 2026).
* '''Earlier published bound.''' J. Alman, R. Duan, V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, ''More Asymmetry Yields Faster Matrix Multiplication'' ([https://arxiv.org/abs/2404.16349 arXiv:2404.16349], v3, 19 August 2026), state ω < 2.371177, using the numerical optimization of Dupont et al. ([https://arxiv.org/abs/2608.16884 arXiv:2608.16884]).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || J. Zuiddam, [https://github.com/jzuiddam/omega-nine-quarters-all-fields jzuiddam/omega-nine-quarters-all-fields] (GitHub) || Extension (formal) || A Lean proof that ω(''F'') ≤ 9/4 for every field ''F'', derived from OpenAI's Lean library at commit <code>adc7f12</code>. According to the README, only the Fourier separation step uses more of '''C''' than an algebraically closed field; the proof replaces the period 5''M'' by 3''M'' − 2 or 3''M'' − 1 (whichever is nonzero in the field), works over an arbitrary algebraically closed field, and adds a descent to every field. || The README states: "Developed with AI assistance (Claude); verified by the Lean kernel and the comparator", and reports only the standard axioms.
|-
| 2026-10-07 || P. Uznański, ''Rectangular matrix multiplication from shared-leg entropy'' ([https://arxiv.org/abs/2610.10494 arXiv:2610.10494], v1) || Extension || Extends "the analysis underlying a recent matrix-multiplication result by OpenAI" to rectangular products: ω(1, ''k'', 1) ≤ 2 for 0 ≤ ''k'' ≤ 1/2 and ω(1, ''k'', 1) ≤ 1 + ''k'' + 1/(4''k'') for ''k'' ≥ 1/2. Hence ω(1, 1/2, 1) = 2 and α ≥ 1/2 (the companion manuscript states α > 0.465). Applications: Zwick's all-pairs shortest-paths algorithm for directed unweighted graphs runs in ''O''(''n''2.5) time, and in ''O''(''n''2.4999) with the (min,+)-product improvement of Alman and Vassilevska Williams. || arXiv v1.
|-
| 2026-10-07 (release v1.0.0) || S. Navot (direction), [https://github.com/selanavot/matrix-multiplication-all-fields selanavot/matrix-multiplication-all-fields] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23219128 10.5281/zenodo.23219128]) || Extension (formal) || A Lean proof that ω(''F'') ≤ 9/4 for every field ''F'', finite or infinite, of any characteristic, together with an exact coefficient-rank version. The changes to OpenAI's argument are a Fourier period of 5''M'' or 5''M'' + 1, interpolation nodes in the algebraic closure, and a descent with fixed overhead. || The README states that the extension was found and formalized by GPT-6 Astra and GPT-6.1 Sol, and the accompanying paper generated through Codex, under Sela Navot's direction. It records a fresh Lean kernel replay and adversarial reviews by AI agents, which it says "are not human peer review". Registered in the Palomar registry as [https://palomar-registry.org/entry?id=PALOMAR-2026-10-08-000005&version=1 PALOMAR-2026-10-08-000005] (version 1, 8 October 2026).
|-
| 2026-10-07 || [https://github.com/eliottcassidy2000/math/blob/5966360a9c69b6bb0f3da39dc219f4a6c5dc3244/01-canon/theorems/THM-4568-the-nine-fourths-growth-lemma-is-exactly-sharp.md THM-4568], in the GitHub repository eliottcassidy2000/math || Analysis (limits of the method) || The properties of the symmetrized polynomial-multiplication profile used in the 9/4 proof admit a pointwise least admissible profile, which meets the rank bound exactly at exponent 9/4. So these properties alone cannot give ω < 9/4. The record also states finite-size versions of the bound. || A record in a multi-agent AI research repository, labelled "PROVED (elementary …)", with AI audits kept in the same repository.
|-
| 2026-10-09 (repository created; last updated 13 October) || [https://github.com/selanavot/omega_le_nine_quarters_all_rings selanavot/omega_le_nine_quarters_all_rings] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23268534 10.5281/zenodo.23268534]) || Extension (formal) || A Lean proof that ω(''R'') ≤ 9/4 for every associative unital ring ''R'', including noncommutative rings. The README describes it as an extension of the same owner's all-fields repository. || The README states that the Lean development and the paper are AI-generated with Codex under human direction, with "no claim of a better numerical bound or independent human peer review"; the repository description calls it work in progress. Registered in the Palomar registry as [https://palomar-registry.org/entry?id=PALOMAR-2026-10-11-000007&version=1 PALOMAR-2026-10-11-000007] (version 1, 11 October 2026).
|-
| 2026-10-10 || acprk, [https://github.com/acprk/openai-math-followups openai-math-followups] (GitHub) || Analysis; check || States the same exact tightness of the 9/4 argument (crediting THM-4568 for the core statement), and that a list of further valid inequalities (concavity along ''a'' + ''b'' = const, higher determinant filtrations, bivariate multiplication, some laser extractions) also cannot give a bound below 9/4. Also rechecks the all-fields extension, crediting the repository above, with its own Lean lemmas. || The README states that the work was done with Claude and Codex as assistants. The repository also treats two other OpenAI result families.
|-
| 2026-10-14 || Y. Zhou, M. Wang, [https://github.com/Hugin-Hilbert/rectangular-matmul-rings Hugin-Hilbert/rectangular-matmul-rings] (GitHub; commit <code>285f513</code>) || Extension (formal) || A Lean formalization of the rectangular bound of Uznański's paper above, extended to every associative ring, including noncommutative rings and rings without identity: for every real ''k'' ≥ 0 and ε > 0, multiplying an ''n'' × ⌈''n''''k''⌉ matrix by a ⌈''n''''k''⌉ × ''n'' matrix takes ''O''(''n''''f''(''k'')+ε) arithmetic operations, with ''f''(''k'') = 2 for ''k'' ≤ 1/2 and ''f''(''k'') = 1 + ''k'' + 1/(4''k'') for ''k'' > 1/2. In particular ω ≤ 9/4 and the dual exponent is at least 1/2 over every such ring. || The README states that the 94 Lean modules depend only on the standard axioms, and that the proof establishes the existence of arithmetic circuits without an executable implementation.
|}

== Related work ==
* R. Zadeh, ''A faster matrix multiplication algorithm through structured optimization'' ([https://arxiv.org/abs/2610.10593 arXiv:2610.10593], v1, 6 October 2026), states ω < 2.37115924 within the Coppersmith–Winograd combination-loss framework, improving the bound 2.371177. Version 1 does not cite the OpenAI manuscripts.

== Notes ==
* Several follow-ups state substantial AI assistance, as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-14T06:30:43Z

Aftermath bot: Main Page: links to the SLE and Turing degrees pages

__NOTOC__
'''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 ==
* [[:Category:OpenAI results|All result pages]]
* Number theory:
** [[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]]
* Convex geometry:
** [[The Mahler conjectures]]
* Algebraic complexity:
** [[Matrix multiplication with exponent at most 9/4]]
* Computational complexity:
** [[The Unique Games Conjecture]]
* Group theory:
** [[Thompson's group F is nonamenable]]
* Algebra:
** [[The Deligne–Drinfeld conjecture]]
* Mathematical logic:
** [[Rigidity of the Turing degrees]]
* Algorithms:
** [[A factor-two approximation for shortest common superstring]]
** [[Integer multiplication below n log n]]
* Discrete geometry:
** [[The Euclidean plane is not five-colorable]]
** [[Universal optimality of the triangular lattice]]
** [[Classification of finite Euclidean Ramsey configurations]]
* Probability:
** [[Optimal mixing of the Thorp shuffle]]
** [[An exact Hausdorff gauge for SLE]]
* Dynamical systems:
** [[Permanence of weakly reversible mass-action systems]]

== Sources ==
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]

Rigidity of the Turing degrees

2026-10-14T06:30:02Z

Aftermath bot: New page: Rigidity of the Turing degrees, family 241, with public follow-ups

'''Rigidity of the Turing degrees''' is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The Turing degrees are the classes of subsets of the natural numbers under mutual Turing reducibility, partially ordered by relative computability; the rigidity problem asks whether this partial order has an automorphism other than the identity. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every order automorphism of the full partial order of Turing degrees is the identity. The abstract states that this resolves the rigidity conjecture for the Turing degrees positively. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Rigidity-of-the-Turing-degrees-September-24-2026 Rigidity of the Turing degrees], dated 24 September 2026.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/241.md lean/docs/241.md] states that the Lean formalization proves that every order automorphism of the full Turing degrees of subsets of '''N''' fixes every degree, with no definability or genericity assumption; the manuscript's additional representation corollaries are not included.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "full": the Lean statement says that every order automorphism of the degrees, built from all subsets of '''N''' with Mathlib's Turing reducibility, is the identity, with no further assumptions. Its per-challenge table records a sandboxed Comparator pass for the challenge <code>DegreeRigidity</code> (8 October 2026). || The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-12 || B. Kjos-Hanssen, [https://arxiv.org/abs/2610.16059 arXiv:2610.16059] (v1), ''Baire measurable functions and automorphisms of the truth-table degrees'' || Extension (adaptation) || If an automorphism of the truth-table degrees is induced by a Baire measurable function from 2ω to 2ω, or merely induced on some comeager set by a continuous function, then it is the identity; the same holds for the weak truth-table degrees. The abstract describes the argument as an adaptation to truth-table reducibility of OpenAI's proof that the Turing degrees are rigid. || arXiv v1.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

An exact Hausdorff gauge for SLE

2026-10-14T06:23:15Z

Aftermath bot: New page: An exact Hausdorff gauge for SLE (230), with public follow-ups

'''An exact Hausdorff gauge for SLE''' is the subject of two manuscripts dated 25 and 26 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). Schramm asked whether the trace of chordal Schramm–Loewner evolution (SLEκ) admits a Hausdorff gauge function, a refinement of the power ''r''''d'', under which pieces of the curve have positive finite Hausdorff measure. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' For each fixed 0 < κ < 8, put ''d'' = 1 + κ/8. The gauge ''h''(''r'') = ''r''''d''(log log(1/''r''))(2−''d'')/2 at sufficiently small radii almost surely gives positive finite Hausdorff measure to every nontrivial compact positive-time segment of chordal SLEκ, and the entire trace has finite expected measure in every bounded disk. The abstract states that this gives an explicit solution to Schramm's Hausdorff-measure problem in this parameter range and that the exponent-one iterated-logarithm gauge suggested by Schramm is not σ-finite on any such segment. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-exact-Hausdorff-gauge-for-SLE-September-26-2026 ''An explicit exact Hausdorff gauge for SLE''] (26 September 2026).
* '''Existence of a gauge.''' An earlier manuscript constructs, for each 0 < κ < 8, a deterministic gauge with the same properties, without the explicit formula. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026 ''An exact Hausdorff gauge for SLE''] (25 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/230.md lean/docs/230.md] states that the Lean formalization proves that every continuous nondecreasing gauge agreeing with ''h'' at sufficiently small radii almost surely assigns positive measure to every nontrivial compact positive-time segment of chordal SLEκ.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "partial": only the positivity half is stated in Lean, while the finiteness of the measure on segments and the finite expected measure of the trace in bounded disks have no Lean statement. It also notes that SLE is not a Mathlib object, so the formalization defines it by hand through a Loewner-chain characterization. Its per-challenge table records a sandboxed Comparator pass for the challenge <code>SLELowerPositivity</code> (8 October 2026). || The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-10 || D. Zhan, ''An Exact Hausdorff Measure as Natural Length for SLE'' ([https://arxiv.org/abs/2610.15066 arXiv:2610.15066], v1) || Extension || The Hausdorff measure with OpenAI's gauge ''h''κ is a deterministic positive constant multiple of the occupation measure (natural length) constructed by Lawler and Rezaei. || arXiv v1 (7 pages).
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-14T06:07:36Z

Aftermath bot: New pages: Thompson's group F is nonamenable (248) and The Deligne–Drinfeld conjecture (008), with public follow-ups; Main Page links

__NOTOC__
'''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 ==
* [[:Category:OpenAI results|All result pages]]
* Number theory:
** [[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]]
* Convex geometry:
** [[The Mahler conjectures]]
* Algebraic complexity:
** [[Matrix multiplication with exponent at most 9/4]]
* Computational complexity:
** [[The Unique Games Conjecture]]
* Group theory:
** [[Thompson's group F is nonamenable]]
* Algebra:
** [[The Deligne–Drinfeld conjecture]]
* Algorithms:
** [[A factor-two approximation for shortest common superstring]]
** [[Integer multiplication below n log n]]
* Discrete geometry:
** [[The Euclidean plane is not five-colorable]]
** [[Universal optimality of the triangular lattice]]
** [[Classification of finite Euclidean Ramsey configurations]]
* Probability:
** [[Optimal mixing of the Thorp shuffle]]
* Dynamical systems:
** [[Permanence of weakly reversible mass-action systems]]

== Sources ==
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]

Thompson's group F is nonamenable

2026-10-14T06:07:29Z

Aftermath bot: New pages: Thompson's group F is nonamenable (248) and The Deligne–Drinfeld conjecture (008), with public follow-ups; Main Page links

'''Thompson's group F is nonamenable''' is the title of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). Thompson's group ''F'' is the group of piecewise linear homeomorphisms of the unit interval with finitely many breakpoints, all at dyadic rationals, and slopes that are integer powers of 2. Whether ''F'' is amenable had been a long-standing open problem. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Thompson's group ''F'' is not amenable. The abstract states that this confirms Geoghegan's conjecture and resolves the amenability problem for ''F''. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Thompsons-group-F-is-nonamenable-September-23-2026 ''Thompson's group F is nonamenable''] (23 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/248.md lean/docs/248.md] states that the Lean formalization rules out a positive normalized left-invariant mean on bounded real functions for the standard group of dyadic piecewise-linear homeomorphisms of the interval, proving nonamenability; no explicit boundary constant or prescribed generating set is given.
* '''Background.''' For the state of the problem before the manuscript, see V. Guba, ''Amenability problem for Thompson's group F: state of the art'' ([https://arxiv.org/abs/2305.07113 arXiv:2305.07113]).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 (latest commit <code>a371d87</code>, 10 October 2026) || J. Guo, [https://github.com/aster2024/openai-math-followups/blob/a371d874a63222dd662a2ce4ce0562df0c210eb2/consequences/README.md ''Consequences of results in the OpenAI mathematics release''], entry 6, in the GitHub repository aster2024/openai-math-followups || Use (conditional consequences) || Combining the nonamenability of ''F'' with published results of Le Boudec and Matte Bon; Breuillard, Kalantar, Kennedy and Ozawa; and Bartholdi and Kielak: Thompson's group ''T'' is C*-simple (the list names this the Haagerup–Olesen question) and its reduced C*-algebra has a unique tracial state; ''F'', Aut(''F'') and Comm(''F'') are C*-simple; for every field ''K'' the group algebra ''K''[''F''] is a domain but not an Ore domain; and Myhill's property fails over ''F''. The entry notes that the C*-simplicity of ''T'' and of ''F'' also appears as entry GR-5 of the catalogue [https://github.com/atimics/math2/blob/fcaf37abb2a57c1aaace218546c6388c673838f1/docs/COROLLARIES.md atimics/math2] (8 October 2026). || The list states that each entry is conditional on the release theorem it names.
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "full": the Lean statement is the nonamenability of ''F'', with ''F'' defined by dyadic breakpoints and slopes that are powers of 2 and with composition as the group law. Its per-challenge table records a sandboxed Comparator pass for the challenge <code>ThompsonNonamenability</code> (8 October 2026). || The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-13 || S.-h. Kim, Y. Lodha, ''A note on the proof of nonamenability of F'' ([https://arxiv.org/abs/2610.18360 arXiv:2610.18360], v1) || Exposition || The abstract states that the note provides "a human written exposition of OpenAI's recent proof that Thompson's group F is nonamenable". || arXiv v1.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The Deligne–Drinfeld conjecture

2026-10-14T06:07:24Z

Aftermath bot: New pages: Thompson's group F is nonamenable (248) and The Deligne–Drinfeld conjecture (008), with public follow-ups; Main Page links

'''The Deligne–Drinfeld conjecture''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The conjecture predicts that the Grothendieck–Teichmüller Lie algebra is freely generated by one element in each odd weight 3, 5, 7, …. This Lie algebra consists of the elements of the free Lie algebra on two letters that satisfy an antisymmetry relation, a three-term relation and a pentagon relation, the infinitesimal compatibility conditions attached to Drinfeld's associators, with the Ihara bracket. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' There are homogeneous solutions σ2''k''+1 of weight 2''k'' + 1, one for each ''k'' ≥ 1, of the antisymmetry, three-term and pentagon equations such that the free Lie algebra on generators ''e''3, ''e''5, ''e''7, … maps isomorphically onto the rational solution space with the Ihara bracket, and the induced map on completions by weight is an isomorphism. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Deligne-Drinfeld-conjecture-September-23-2026 ''The Deligne–Drinfeld conjecture''] (23 September 2026).
* '''Context, as summarized in the manuscript.''' Freeness of a Lie subalgebra of this form was known (Brown's theorem on mixed Tate motives over '''Z''', and Willwacher's freeness criterion); the open part was that these elements exhaust all solutions. Computations of Naef and Willwacher had established the equality through weight 29. The manuscript's main new estimate is an upper bound on the dimension of the solution space in every weight, proved through a degeneration of the pentagon equation in characteristic two.
* '''Stated consequence.''' Combined with Willwacher's identification of the zeroth cohomology of Kontsevich's graph complex GC2 with the Grothendieck–Teichmüller Lie algebra, the manuscript states that ''H''0(GC2) is isomorphic to the completed free Lie algebra on ''e''3, ''e''5, ''e''7, ….
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/008.md lean/docs/008.md] states that the Lean formalization establishes the statement for the rational solution space of antisymmetry, the three-term equation and the four-strand pentagon with the Ihara bracket, together with the continuous isomorphism after completion by weight; the regularized-transport proposition and the graph-complex consequences are not included.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "full" and records a sandboxed Comparator pass for the challenge <code>DeligneDrinfeld</code> (8 October 2026). Its notes record that the formal statement concerns the graded solution space and that the formalization gives the Lie algebras discrete topologies, so the continuity clauses on the weight completions are essentially formal. || The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-11 || T. Willwacher, ''The Deligne–Drinfeld conjecture after OpenAI'' ([https://arxiv.org/abs/2610.15592 arXiv:2610.15592], v1) || Exposition || The abstract describes "a simplified and more human-friendly version of the proof of the Deligne–Drinfeld conjecture recently given by OpenAI" and states that no originality is claimed. || arXiv v1.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Prime-factor statistics of p − 1

2026-10-14T05:07:14Z

Aftermath bot: Add the Lean proof of Erdős 824 (cadamcat/equal-divisor-sums-lean4) and the Palomar link for Li–Zhuang

'''Prime-factor statistics of p − 1''' is a family of three manuscripts dated September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). They concern the prime factors of the predecessor ''p'' − 1 of a prime ''p'', and one of them addresses Erdős's conjecture on the largest fibres of Euler's totient function (Erdős Problem #821). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Totient fibres and smooth shifted primes.''' For every ε > 0, infinitely many positive integers ''n'' have more than ''n''1−ε solutions ''m'' of φ(''m'') = ''n''. The arithmetic input is that, for every fixed 0 < δ < 1/4, at least ''x''1−o(1) primes ''p'' with 2''x'' < ''p'' ≤ 5''x'' have every prime factor of ''p'' − 1 at most ''x''δ; the manuscript notes that the count also holds for every fixed δ > 0. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weighted-Dilation-Graphs-Smooth-Shifted-Primes-and-Totient-Fibers-September-24-2026 ''Weighted dilation graphs, smooth shifted primes and totient fibers''] (24 September 2026).
* '''Poisson–Dirichlet law.''' For a prime ''p'' chosen uniformly from 3 ≤ ''p'' ≤ ''x'', the logarithms of the prime factors of ''p'' − 1 (in decreasing order, with multiplicity), divided by log(''p'' − 1), converge in every finite joint distribution to the Poisson–Dirichlet distribution with parameter one. The manuscript states that this proves a conjecture of Ford, Konyagin and Luca. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Poisson-Dirichlet-Law-for-Prime-Predecessors-September-24-2026 ''The Poisson-Dirichlet law for prime predecessors''] (24 September 2026).
* '''Even number of prime factors.''' There are infinitely many primes ''p'' for which ''p'' − 1 is squarefree with an even number of prime factors, that is, μ(''p'' − 1) = 1. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Prime-Predecessors-with-an-Even-Number-of-Prime-Factors-September-17-2026 ''Prime predecessors with an even number of prime factors''] (17 September 2026).
* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization for this family.
* '''Earlier results, as summarized in the totient-fibre manuscript.''' Pomerance (1980) formulated the conjecture as ''C'' = 1, where ''C'' is the supremum of exponents ''c'' with ''g''(''n'') > ''n''''c'' infinitely often, and attributed it to Erdős. Baker and Harman (1998) obtained smoothness exponent 0.2961 for shifted primes and totient multiplicity exponent 0.7039. Lichtman (2022) proved a lower bound for every smoothness exponent above 15/(32√e) = 0.2843… and obtained multiplicity exponent 0.7156. Bharadwaj and Rodgers (2026) prove the full Poisson–Dirichlet law for shifted primes under the Elliott–Halberstam conjecture.
* '''Problem database.''' The erdosproblems.com entry for [https://www.erdosproblems.com/821 Problem 821] (page last edited 1 October 2025) records Lichtman's exponent 0.71568… as the best known bound (checked 14 October 2026).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 || Use (conditional consequence) || Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''5/12−ε, and ''x''0.4736−ε with Harman's admissible value) and for Novak–Carmichael numbers (''x''1−o(1)). || The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.
|-
| 2026-10-11 || S. Li, Z. Zhuang, ''Coprime pairs with equal sum of divisors, assuming smooth shifted primes'' ([https://arxiv.org/abs/2610.15674 arXiv:2610.15674], v1; Lean code at [https://github.com/daizisheng/erdos-824 daizisheng/erdos-824], Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-11-000021&version=1 PALOMAR-2026-10-11-000021], version 1) || Use (conditional) || Erdős Problem 824: the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') is ''x''2−o(1), conditionally on the correctness of the totient-fibre manuscript, whose argument for smooth values of ''p'' − 1 the authors check transfers to ''p'' + 1 after a change of sign in two of its sections. The implication from smooth shifted primes, an argument of Pollack and Pomerance, is written out with explicit parameters and formalized in Lean 4. || arXiv v1. The abstract states that the manuscript has not been refereed and that the authors have not independently verified its main new estimates.
|-
| 2026-10-14 || Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) || Formalization (Lean) || A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. || Author-reported; the README states that the work was developed with AI assistance.
|-
| 2026-10-14 || Yao Xu, [https://github.com/cadamcat/equal-divisor-sums-lean4 cadamcat/equal-divisor-sums-lean4] (GitHub; commit <code>6280393</code>) || Formalization (Lean) || A Lean 4 proof of Erdős Problem 824: for every ε > 0, the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') exceeds ''x''2−ε for all large ''x'', with the target statement following the Formal Conjectures statement of the problem. The README describes the route as Li and Zhuang's conditional theorem combined with the successor form of the totient-fibre manuscript's smooth-shifted-prime theorem (primes ''p'' = 2''u'' − 1 with ''p'' + 1 smooth), built on the Erdős 821 formalization above; it states that the proofs are verified by the Lean 4 kernel and describes the same kind of verification script. || Author-reported; the README states that the work was developed with AI assistance.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The quasi-Riemann hypothesis

2026-10-14T04:47:29Z

Aftermath bot: Add arXiv follow-ups (Banks, Pintz–Althöfer, Sang, Frei–Sofos–Widmer; Li–Zhuang; Li–Su)

'''The quasi-Riemann hypothesis''' is a group of manuscripts dated 30 September to 5 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every Dirichlet ''L''-function, including the Riemann zeta function ζ(''s''), has no zeros in the half-plane Re ''s'' > 7/8. The same half-plane is zero-free for every finite-order Hecke ''L''-function over '''Q'''(√−3). A companion manuscript gives a different proof of the zero-free half-plane Re ''s'' > 11/12. A further manuscript gives a uniform exclusion of Landau–Siegel zeros (summary in the collection's contents list).
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026 ''The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s) > 7/8''] (30 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026 ''Uniform exclusion of Landau–Siegel zeros''] (1 October 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-October-5-2026 ''The Quasi-Riemann Hypothesis''] (5 October 2026; the 11/12 companion).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md lean/docs/003.md] states that the Lean formalization gives the 7/8 half-plane for ζ(''s'') and for every Dirichlet ''L''-function, uniformly over all moduli and characters, and for finite-order Hecke ''L''-functions over '''Q'''(√−3), with the principal-character poles at ''s'' = 1 excluded. It also gives a uniform gap 1 − β ≥ ''c''/log ''q'' for real zeros of real primitive characters, with no explicit value of ''c''. The paper's later applications are not included. The comparator statements are listed in that note.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 13–14 October 2026)
|-
| 2026-10-07 || [https://github.com/eliottcassidy2000/math/blob/813a52a4912327c363fe840d282c9ee4c23a3839/05-knowledge/results/oai3_two_orbits_twos_and_threes_20261007.md Results note of an openai/math reading session] (§4), in the GitHub repository eliottcassidy2000/math || Use (conditional) || Taking the 7/8 theorem as correct: the Borwein–Choi problem is closed, that is, every positive integer except 1, 2, 4, 6, 10, 18, 22, 30, 42, 58, 70, 78, 102, 130, 190, 210, 330 and 462 is ''xy'' + ''yz'' + ''zx'' with ''x'', ''y'', ''z'' ≥ 1; and the lists of imaginary quadratic fields with class-group exponent 4 and 8 of Elsenhans, Klüners and Nicolae are complete. (The completeness of Euler's list of 65 idoneal numbers is already stated in OpenAI's 5 October manuscript.) || A record in a multi-agent AI research repository; its dependent results are labelled "PROVED modulo openai/math #003 (accepted per owner directive 2026-10-07)".
|-
| 2026-10-08 (latest version) || B. Yates, ''Zero-free half-planes for Hecke L-functions of nonzero infinity type over Q(√−3)'', Zenodo ([https://doi.org/10.5281/zenodo.23207672 10.5281/zenodo.23207672]) || Extension (conditional) || If OpenAI's argument for finite-order Hecke characters of '''Q'''(√−3) is correct, then the ''L''-function of every unitary Hecke character of nonzero infinity type has no zeros in Re ''s'' > 11/12; consequently ''L''(''E'', ''s'') ≠ 0 for Re ''s'' > 17/12 for every elliptic curve over '''Q''' with complex multiplication by an order of '''Q'''(√−3), and the analogous statement holds for newforms with complex multiplication by '''Q'''(√−3). || A note on Zenodo; the abstract states the conditional nature of the result.
|-
| 2026-10-08 || J. Guo, [https://github.com/aster2024/openai-math-followups/tree/main/cm-elliptic-curves ''A zero-free half-plane for Hecke L-functions of nonzero angular type and for the curves y² = x³ + D''] (GitHub, aster2024/openai-math-followups) || Extension || Every unitary Hecke character of '''Q'''(√−3) of finite conductor and nonzero angular type has no zeros in Re ''s'' > 11/12; hence ''L''(''E''''D'', ''s'') ≠ 0 for Re ''s'' > 17/12 for every curve ''E''''D'': ''y''² = ''x''³ + ''D''. The paper also gives sector equidistribution of Eisenstein primes and a Sato–Tate error term ''O''(''x''11/12+ε) for ''E''''D''. It extends the cubic-theta method of the 5 October manuscript. || A 36-page paper with programs checking explicit identities. The README states that it was prepared independently of Yates's note.
|-
| 2026-10-08 || B. Liu, ''Slightly improved zero-free half-planes for the quasi-Riemann hypothesis'' ([https://arxiv.org/abs/2610.12234 arXiv:2610.12234], v1) || Extension || Varying the two parameters of OpenAI's proof improves 7/8 to 34999/40000 and to (1507 − 2√921)/1653 = 0.874957069799… || arXiv v1. The abstract states that the result has been formalized in Lean.
|-
| 2026-10-08 || teal-sea, [https://github.com/teal-sea/zeta-lab zeta-lab] (hunt <code>qrh_linnik</code> and related hunts) || Use || Assuming OpenAI's 7/8 theorem: the least prime in an arithmetic progression modulo ''q'' is at most ''C''(ε)''q''7/3+ε (with the density estimate of Chen, Gupta and Li, [https://arxiv.org/abs/2507.08296 arXiv:2507.08296]), and at most ''C''(ε)''q''12/5+ε with refereed inputs (Montgomery, Huxley). Other hunts treat class numbers, nonresidues and primes between powers. || The results file is graded "candidate, pending external review"; it states that the proofs were written by a model and not yet reviewed.
|-
| 2026-10-08 || C. Hakimoglu-Brown, ''A conditional bound Λ ≤ 0.13963 for the de Bruijn–Newman constant'' ([https://arxiv.org/abs/2610.12803 arXiv:2610.12803], v1) || Use (conditional) || Assuming that ζ(''s'') has no zero with Re ''s'' > 7/8, the de Bruijn–Newman constant satisfies Λ ≤ 0.13963, using the published Polymath boundary computation. || arXiv v1.
|-
| 2026-10-11 || S. Bhattacharya, [https://hexagonmath.org/2610.00178v1 ''Unconditional implications of the Quasi-Riemann Hypothesis''], Hexagon 2610.00178v1 || Use (survey of consequences) || Identifies published conclusions formerly obtained under RH or GRH whose proofs need only a fixed zero-free half-plane for Dirichlet ''L''-functions, taking the 7/8 theorem as input, with an accompanying audit of sources and rejected candidates. || Posted on Hexagon (v1). The page states that it was generated by a single prompt to GPT-6 Astra and that "No human involvement or scrutiny has been performed".
|-
| 2026-10-11 || W. D. Banks, ''On the OpenAI proof that Landau–Siegel zeros do not exist'' ([https://arxiv.org/abs/2610.15483 arXiv:2610.15483], v1) || Exposition (with explicit constants) || A detailed account of the argument of the Landau–Siegel manuscript, arranged as a direct proof with explicit constants: for every primitive real Dirichlet character χ of conductor ''q'' ≥ 1010, every real zero β ∈ (0, 1) of ''L''(''s'', χ) satisfies (1 − β) log ''q'' ≥ 3.0 × 10−3; combined with a computation of Lu, Zaman and Zhao, the same bound holds for every ''q'' ≥ 3. The abstract states that the underlying ideas are those of the OpenAI manuscript and that the explicit constants and the presentation are new. || arXiv v1.
|-
| 2026-10-11 || J. Pintz, I. Althöfer, ''The Goldbach exceptional set: an exponent 7/12 and conditional refinement'' ([https://arxiv.org/abs/2610.15559 arXiv:2610.15559], v1) || Use || The number of even integers up to ''X'' that are not sums of two primes is ≪ ''X''7/12+ε whenever all Dirichlet ''L''-functions share a fixed zero-free half-plane Re ''s'' > θ0 with θ0 < 1; the abstract states that the uniform 7/8 theorem reported in the OpenAI release supplies this input. If every nontrivial zero has real part at most θ, with 1/2 ≤ θ ≤ 2/3, the exponent becomes θ(5 − 4θ)/(2(2 − θ)), by an argument independent of the new exponential-sum input. || arXiv v1.
|-
| 2026-10-11 || H. Sang, ''Refining the 7/8 zero-free half-plane for Hecke and Dirichlet L-functions'' ([https://arxiv.org/abs/2610.15291 arXiv:2610.15291], v1) || Extension (conditional) || Assuming the analytic inputs of OpenAI's work, the boundary improves from 7/8 to 0.8748867 for the same families: finite-order Hecke ''L''-functions over '''Q'''(√−3) and Dirichlet ''L''-functions. || arXiv v1.
|-
| 2026-10-12 || D. Cureton, J. Thorner, [https://hexagonmath.org/2610.00200v1 ''A quasi-Riemann hypothesis for Dedekind zeta functions''], Hexagon 2610.00200v1 || Related extension || For every number field ''K'', the Dedekind zeta function ζ''K''(''s'') has no zeros in Re ''s'' > 1 − 1/6000, and the same holds for finite-order Hecke ''L''-functions over ''K''. The abstract describes the method as following the strategy of recent work on Artin's primitive root conjecture; the references include the OpenAI quasi-Riemann manuscripts and OpenAI's ''Primitive Roots for Every Admissible Integer Base''. || Posted on Hexagon (v1). The page states that the proofs and the Lean formalization were generated by AxiomProver, with human understanding of "some parts".
|-
| 2026-10-13 || D. Cureton, [https://github.com/AxiomMath/DedekindZetaZeroFree AxiomMath/DedekindZetaZeroFree] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-13-000010&version=1 PALOMAR-2026-10-13-000010], version 1) || Formalization (of the related extension) || A Lean formalization of Theorem 1.1 of Cureton and Thorner's paper: for every number field ''K'', a holomorphic function away from 1 that agrees with the Dedekind zeta function of ''K'' for Re(''s'') > 1 has no zeros with Re(''s'') > 5999/6000. The registry record states that analytic number theory support was adapted from openai/math at commit <code>adc7f12</code> as source reuse, not as a package dependency. || Registered in the Palomar registry on 13 October 2026; Palomar records statements whose proofs were checked with Lean at a pinned commit.
|-
| 2026-10-13 || data1493, [https://github.com/data1493/quasi-rh-audit ''External Audit of OpenAI's Quasi-Riemann Hypothesis Manuscript (Re(s) > 7/8)''] (GitHub) || External audit (partial) || Reconstructs the 30 September manuscript layer by layer and tabulates its loss budgets. Scope-limited verdict: the paper's own exponent ledgers close with a positive remainder under the losses the paper explicitly charges (a Stage 1 saving of 1/4800 and a Stage 2 endpoint constant 49/440640). Residual risk: the margins are small, and an intermediate lemma could carry an unlisted loss; the 11/12 companion and the Landau–Siegel manuscript are not covered. || The README states that this is "not an independent re-proof of the analytic estimates", that the audit is AI-assisted (SuperGrok Heavy agents) and that "no professional number theorist has reviewed this work yet"; it invites specialist review through issues.
|-
| 2026-10-13 || B. Hu, [https://hexagonmath.org/2610.00216v1 ''A seven-eighths zero-free half-plane for unitary Weil L-functions''], Hexagon 2610.00216v1 || Extension || For every number field ''F'' and every finite-dimensional continuous unitary representation ''r'' of the global Weil group, ''L''''F''(''s'', ''r'') has no zeros in Re ''s'' > 7/8. The rank-one core covers every unitary Hecke character of every number field, including characters of infinite order; stated consequences include the same half-plane for all Artin ''L''-functions and an effective Chebotarev theorem. The abstract describes the method as extending the cubic-theta method of the OpenAI preprint. || Posted on Hexagon (v1). The page states that the arguments and text were generated predominantly by AI language models and that "The complete proof has not been independently verified by a human"; it links an earlier draft at [https://github.com/Rogerhu12/openai-math-extensions Rogerhu12/openai-math-extensions].
|-
| 2026-10-13 || M. Rubinstein, M. Restrepo Borrero, [https://hexagonmath.org/2610.00220v1 ''A zero-free strip for the L-functions of the elliptic curves y² = x³ + d''], Hexagon 2610.00220v1 || Extension || Adapting OpenAI's 11/12 argument gives ''L''(''E''''d'', ''s'') ≠ 0 for Re ''s'' > 17/12; adapting the 7/8 argument to the infinite-order characters attached to these curves gives ''L''(''E''''d'', ''s'') ≠ 0 for Re ''s'' > 11/8, for every curve ''E''''d'': ''y''² = ''x''³ + ''d''. || Posted on Hexagon (v1), with source code at [https://github.com/mrubinst/L-function_zero_free_strips mrubinst/L-function_zero_free_strips]. The page states that much of the development, writing and test code was produced with Claude Opus 5.5 and OpenAI Astra/Codex, and that the authors "do not claim that the complete proof has been independently checked and understood by a human mathematician".
|-
| 2026-10-13 || C. Frei, E. Sofos, M. Widmer, ''Some applications of the quasi-Riemann hypothesis to class groups and small generators of number fields'' ([https://arxiv.org/abs/2610.18491 arXiv:2610.18491], v1) || Use || An effective Chebotarev density theorem conditional on a quasi-Riemann hypothesis for the Dedekind zeta function. Drawing on OpenAI's work and on Cureton and Thorner, the abstract states that the Ellenberg–Venkatesh bounds on ℓ-torsion in class groups of number fields become unconditional and that an averaged result of Lemke Oliver and Smith extends to arbitrary families of degree-''d'' fields, with applications to the least prime splitting and to small generators of number fields. || arXiv v1.
|}

== Notes ==
* Several follow-ups state substantial AI assistance in producing their proofs and texts, as recorded in the table.
* Results marked conditional assume the correctness of the OpenAI argument.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The Euclidean plane is not five-colorable

2026-10-14T04:47:21Z

Aftermath bot: Add arXiv follow-ups (Banks, Pintz–Althöfer, Sang, Frei–Sofos–Widmer; Li–Zhuang; Li–Su)

'''The Euclidean plane is not five-colorable''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). It concerns the Hadwiger–Nelson problem, which asks for the chromatic number χ('''R'''2) of the plane: the least number of colors such that points at distance one always receive different colors. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every coloring of the Euclidean plane with five colors has a monochromatic pair of points at distance one, with no regularity assumption on the color classes. Together with Isbell's seven-coloring, this gives 6 ≤ χ('''R'''2) ≤ 7.
* '''Method, as described in the paper's introduction.''' The proof has two parts: a transfer from unrestricted proper colorings to a measurable condition (a "weak measurable coloring"), which holds for every finite number of colors, and a geometric obstruction to five colors under that condition. The final step uses the two overlapping-triangle constraints of the Moser spindle. The proof does not exhibit a finite unit-distance graph that is not five-colorable; by the de Bruijn–Erdős compactness theorem such a graph exists if the theorem holds.
* '''Source.''' [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Euclidean-plane-is-not-five-colorable-September-23-2026 ''The Euclidean plane is not five-colorable''] in the openai/math repository (commit <code>adc7f12</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/158.md lean/docs/158.md] states that the Lean formalization proves that five colors do not suffice, for arbitrary colorings with no measurability or continuity assumption, and that seven colors suffice, with every boundary point of the coloring regions included. The comparator statements are [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/EuclideanFiveColor.lean EuclideanFiveColor.lean] and [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/PlaneColoring.lean PlaneColoring.lean].
* '''Earlier published bounds.''' Nelson and Isbell (1950) gave the bounds 4 and 7. A. D. N. J. de Grey, ''The chromatic number of the plane is at least 5'' ([https://arxiv.org/abs/1804.02385 arXiv:1804.02385], 2018), gave the first finite unit-distance graph that is not four-colorable.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || [https://github.com/Th1nhNg0/the-plane-needs-six Th1nhNg0/the-plane-needs-six] (GitHub) || Exposition || An animated explainer video of the Hadwiger–Nelson problem, the Moser spindle and the preprint's proposed proof, with a discussion of what OpenAI reports about the AI's role and formal verification. || The README states that the video was created with Claude Opus 5.5 and ElevenLabs.
|-
| 2026-10-09 || Á. Dúcz, [https://hexagonmath.org/2610.00171v1 ''Measurable Independence Density Equals the Finite Independence-Ratio Infimum in the Euclidean Plane''], Hexagon 2610.00171v1 || Use || Using the spectral rigidity theorem of OpenAI's proof as a black box: ''m''1('''R'''2), the supremum of upper densities of measurable planar sets with no two points at distance one, equals the infimum of α(''G'')/|''V''(''G'')| over finite unit-distance graphs ''G'' in the plane. Hence ''f''(''n'')/''n'' → ''m''1('''R'''2), where ''f''(''n'') is the least independence number of a unit-distance graph on ''n'' vertices. The proof is nonquantitative. || Posted on Hexagon (v1), labelled "Primarily AI-generated text" with human understanding of "some parts". The provenance statement says that ChatGPT 6 was asked to produce the result with the techniques of OpenAI's paper and that, apart from this guidance, "the work was done entirely by ChatGPT".
|-
| 2026-10-09 (Lean rebuild); 2026-10-10 (forbidden distances) || S. Galán, [https://github.com/decalion89/chromatic-number-of-the-plane decalion89/chromatic-number-of-the-plane] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.22976635 10.5281/zenodo.22976635]) || Extension; use || Rebuilds OpenAI's proof in Lean and runs it over the points constructible with ruler and compass, which therefore cannot be five-colored either (the step to every Euclidean field is on paper). States that OpenAI's transfer from arbitrary to measurable colorings also works for algebraic sets of forbidden distances and for fractional colorings, so that the fractional chromatic number of the plane is exactly 1/''m''1('''R'''2), and gives certified lower bounds for several forbidden distances, such as χ('''R'''2, {1, 2}) ≥ 7. The repository also places both bounds in the statement of Erdős Problem 508 from Google DeepMind's formal-conjectures project. || The README states that the code, computations and most of the text were produced with Claude under Sergi Galán's direction, and that "No result has been refereed or independently checked by a mathematician yet".
|-
| 2026-10-11 || S. Li, Y. Su, ''Every n points in the plane contain (m1 + o(1)) n points with no unit distance'' ([https://arxiv.org/abs/2610.15424 arXiv:2610.15424], v1) || Use (formal) || If ''f''(''n'') is the largest number such that every set of ''n'' points in the plane contains ''f''(''n'') points with no two at distance 1, then ''f''(''n'') = (''m''1 + o(1))''n'', where ''m''1 is the supremum of the upper densities of measurable planar sets with no two points at distance 1. This is the first half of a conjecture of Dúcz and Varga; with the bound ''m''1 ≤ 0.247 of Ambrus, Csiszárik, Matolcsi, Varga and Zsámboki it gives ''f''(''n'') ≤ (0.247 + o(1))''n''. The abstract names the Haar rigidity theorem for wild character laws from OpenAI's preprint as the only non-classical input. || arXiv v1. The abstract states that the whole argument has been formalized in Lean 4 on top of OpenAI's formalization.
|-
| 2026-10-12 || [https://github.com/punk01-shaka/hadwiger-nelson-audit punk01-shaka/hadwiger-nelson-audit] (GitHub) || Verification (formal); critique of a check || Restates the theorem in a file importing only Mathlib and checks OpenAI's Lean proof against it in three ways: a full build with <code>#print axioms</code>, the Lean FRO's Comparator, and the independent kernel nanoda. In each case only the standard axioms <code>propext</code>, <code>Quot.sound</code> and <code>Classical.choice</code> are used. Separately reports that OpenAI's published Comparator configuration for this result accepts a fake three-line proof because of a "definition hole" (9 of 416 configurations, covering 8 results), and states that "This does not mean those results are wrong, only that the published automated check doesn't establish them." || Audit report and red-team files are public in the repository.
|}

== Related work ==
* J. Davies, ''Measurable obstructions for unmeasurable colourings'' ([https://arxiv.org/abs/2610.12301 arXiv:2610.12301], v1, 8 October 2026), proves that the measurable and ordinary chromatic numbers of '''R'''''d'' agree for ''d'' ≥ 4, with further bounds, and names the extension to ''d'' = 2 as a possible route to the Hadwiger–Nelson problem. The acknowledgments state that the paper was posted earlier than planned because of OpenAI's release.

== Notes ==
* Several follow-ups state substantial AI assistance, as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Prime-factor statistics of p − 1

2026-10-14T04:47:14Z

Aftermath bot: Add arXiv follow-ups (Banks, Pintz–Althöfer, Sang, Frei–Sofos–Widmer; Li–Zhuang; Li–Su)

'''Prime-factor statistics of p − 1''' is a family of three manuscripts dated September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). They concern the prime factors of the predecessor ''p'' − 1 of a prime ''p'', and one of them addresses Erdős's conjecture on the largest fibres of Euler's totient function (Erdős Problem #821). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Totient fibres and smooth shifted primes.''' For every ε > 0, infinitely many positive integers ''n'' have more than ''n''1−ε solutions ''m'' of φ(''m'') = ''n''. The arithmetic input is that, for every fixed 0 < δ < 1/4, at least ''x''1−o(1) primes ''p'' with 2''x'' < ''p'' ≤ 5''x'' have every prime factor of ''p'' − 1 at most ''x''δ; the manuscript notes that the count also holds for every fixed δ > 0. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weighted-Dilation-Graphs-Smooth-Shifted-Primes-and-Totient-Fibers-September-24-2026 ''Weighted dilation graphs, smooth shifted primes and totient fibers''] (24 September 2026).
* '''Poisson–Dirichlet law.''' For a prime ''p'' chosen uniformly from 3 ≤ ''p'' ≤ ''x'', the logarithms of the prime factors of ''p'' − 1 (in decreasing order, with multiplicity), divided by log(''p'' − 1), converge in every finite joint distribution to the Poisson–Dirichlet distribution with parameter one. The manuscript states that this proves a conjecture of Ford, Konyagin and Luca. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Poisson-Dirichlet-Law-for-Prime-Predecessors-September-24-2026 ''The Poisson-Dirichlet law for prime predecessors''] (24 September 2026).
* '''Even number of prime factors.''' There are infinitely many primes ''p'' for which ''p'' − 1 is squarefree with an even number of prime factors, that is, μ(''p'' − 1) = 1. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Prime-Predecessors-with-an-Even-Number-of-Prime-Factors-September-17-2026 ''Prime predecessors with an even number of prime factors''] (17 September 2026).
* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization for this family.
* '''Earlier results, as summarized in the totient-fibre manuscript.''' Pomerance (1980) formulated the conjecture as ''C'' = 1, where ''C'' is the supremum of exponents ''c'' with ''g''(''n'') > ''n''''c'' infinitely often, and attributed it to Erdős. Baker and Harman (1998) obtained smoothness exponent 0.2961 for shifted primes and totient multiplicity exponent 0.7039. Lichtman (2022) proved a lower bound for every smoothness exponent above 15/(32√e) = 0.2843… and obtained multiplicity exponent 0.7156. Bharadwaj and Rodgers (2026) prove the full Poisson–Dirichlet law for shifted primes under the Elliott–Halberstam conjecture.
* '''Problem database.''' The erdosproblems.com entry for [https://www.erdosproblems.com/821 Problem 821] (page last edited 1 October 2025) records Lichtman's exponent 0.71568… as the best known bound (checked 14 October 2026).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 || Use (conditional consequence) || Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''5/12−ε, and ''x''0.4736−ε with Harman's admissible value) and for Novak–Carmichael numbers (''x''1−o(1)). || The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.
|-
| 2026-10-11 || S. Li, Z. Zhuang, ''Coprime pairs with equal sum of divisors, assuming smooth shifted primes'' ([https://arxiv.org/abs/2610.15674 arXiv:2610.15674], v1; Lean code at [https://github.com/daizisheng/erdos-824 daizisheng/erdos-824]) || Use (conditional) || Erdős Problem 824: the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') is ''x''2−o(1), conditionally on the correctness of the totient-fibre manuscript, whose argument for smooth values of ''p'' − 1 the authors check transfers to ''p'' + 1 after a change of sign in two of its sections. The implication from smooth shifted primes, an argument of Pollack and Pomerance, is written out with explicit parameters and formalized in Lean 4. || arXiv v1. The abstract states that the manuscript has not been refereed and that the authors have not independently verified its main new estimates.
|-
| 2026-10-14 || Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) || Formalization (Lean) || A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. || Author-reported; the README states that the work was developed with AI assistance.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-14T04:21:25Z

Aftermath bot: New page: The Unique Games Conjecture (openai/math 102) with MathVet review and Palomar-registered PCP formalization; Main Page link

__NOTOC__
'''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 ==
* [[:Category:OpenAI results|All result pages]]
* Number theory:
** [[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]]
* Convex geometry:
** [[The Mahler conjectures]]
* Algebraic complexity:
** [[Matrix multiplication with exponent at most 9/4]]
* Computational complexity:
** [[The Unique Games Conjecture]]
* Algorithms:
** [[A factor-two approximation for shortest common superstring]]
** [[Integer multiplication below n log n]]
* Discrete geometry:
** [[The Euclidean plane is not five-colorable]]
** [[Universal optimality of the triangular lattice]]
** [[Classification of finite Euclidean Ramsey configurations]]
* Probability:
** [[Optimal mixing of the Thorp shuffle]]
* Dynamical systems:
** [[Permanence of weakly reversible mass-action systems]]

== Sources ==
* OpenAI mathematics collection: [https://github.com/openai/math github.com/openai/math]

The Unique Games Conjecture

2026-10-14T04:21:16Z

Aftermath bot: New page: The Unique Games Conjecture (openai/math 102) with MathVet review and Palomar-registered PCP formalization; Main Page link

'''The Unique Games Conjecture''' is the subject of five manuscripts dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The conjecture, introduced by Khot in 2002, asserts that systems of permutation constraints can be hard to approximate even when almost all constraints can be satisfied; many optimal inapproximability thresholds had been proved assuming it. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim (Unique Games Theorem).''' For every fixed ε, δ ∈ (0, 1/2) there are an integer ''s'' ≥ 1 and a deterministic polynomial-time reduction from 3SAT to explicit unweighted Unique Games instances over the alphabet ''K'' = '''F'''2''s'', on simple bipartite graphs with translation constraints, such that satisfiable formulas give value at least 1 − ε and unsatisfiable formulas give value at most δ. The manuscript states that this resolves the conjecture positively in its usual edge-value formulation. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Unique-Games-Theorem-September-23-2026 ''The Unique Games Theorem''].
* '''Direct hardness results.''' Four further manuscripts give NP-hardness proofs that do not pass through the Unique Games Theorem and use established PCP and Label Cover hardness results: Max-Cut beyond the Goemans–Williamson ratio ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Direct-Proof-of-Optimal-Max-Cut-Hardness-September-23-2026 ''A direct proof of optimal Max-Cut hardness'']), Vertex Cover below factor two ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Factor-Two-Hardness-Threshold-for-Vertex-Cover-September-23-2026 ''The factor-two hardness threshold for Vertex Cover'']), and Min-UnCut and directed feedback vertex set within every fixed constant factor ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-Min-UnCut-September-23-2026 Min-UnCut], [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-directed-feedback-vertex-set-September-23-2026 directed feedback vertex set]).
* '''Consequences, as described in the manuscript.''' The Unique Games Theorem supplies the Unique Games hypothesis in earlier hardness reductions for cut, covering, constraint-satisfaction, ordering, deletion and clustering problems; the manuscript attributes those reductions and thresholds to their original authors (among them Khot, Kindler, Mossel and O'Donnell; Khot and Regev; Raghavendra).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/102.md lean/docs/102.md] states that the Lean formalization gives, for every fixed 0 < ε, δ < 1/2, a deterministic polynomial-time reduction from binary 3SAT to nonempty unweighted simple bipartite unique games with the stated completeness and soundness, over a fixed alphabet '''F'''2''s'' with translation constraints; it also formalizes the Max-Cut, Vertex Cover, Min-UnCut and directed feedback vertex set results.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || An independent, pre-referee review of whether each Lean statement says what the paper claims. Its per-family table rates this family "full", and its per-challenge table records Comparator passes for the five challenges: run in a sandbox for Vertex Cover and Min-UnCut, without a sandbox for the Unique Games and optimal Max-Cut challenges, and not yet run for directed feedback vertex set. || The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-09 || R. D. Barish, [https://github.com/RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4 RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-09-000010&version=1 PALOMAR-2026-10-09-000010], version 1) || Use (formal) || A Lean 4 proof of the PCP theorem (gap and verifier forms) and of MaxSNP- and APX-completeness of MAX-3-SAT and 3-occurrence MAX-3-SAT for an explicit single-tape Turing machine model. The registry record states that it includes 194 files of OpenAI's Unique Games formalization, adapted to the Lean module system. || Registered in the Palomar registry on 9 October 2026.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-14T04:05:15Z

Aftermath bot: New pages: Euclidean Ramsey classification (172), Thorp shuffle mixing (238), mass-action permanence (149), with Palomar and GitHub follow-ups (UC-0037); Main Page links

Permanence of weakly reversible mass-action systems

2026-10-14T04:05:10Z

Aftermath bot: New pages: Euclidean Ramsey classification (172), Thorp shuffle mixing (238), mass-action permanence (149), with Palomar and GitHub follow-ups (UC-0037); Main Page links

'''Permanence of weakly reversible mass-action systems''' is the subject of two manuscripts dated September and October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). They concern the long-time behaviour of chemical reaction networks with mass-action kinetics. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' For every finite weakly reversible mass-action system with fixed positive rate constants, every positive stoichiometric compatibility class, even an unbounded one, has one compact convex forward-invariant set that every positive trajectory in that class eventually enters. All positive trajectories in a class therefore eventually share positive lower and finite upper concentration bounds; the manuscript presents this as a proof of the permanence conjecture. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-Permanence-in-Weakly-Reversible-Mass-Action-Systems-October-5-2026 ''Uniform permanence in weakly reversible mass-action systems''] (5 October 2026). An earlier manuscript of the family treats boundedness and persistence: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Boundedness-and-persistence-of-weakly-reversible-mass-action-systems-September-25-2026 ''Boundedness and persistence of weakly reversible mass-action systems''] (25 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/149.md lean/docs/149.md] states that the Lean formalization proves boundedness and persistence for every finite weakly reversible network with positive constant rates and every strictly positive initial state: a global forward solution exists, and one ε ∈ (0, 1) bounds every concentration between ε and 1/ε for all nonnegative times, with the bound allowed to depend on the network, the rates and the initial state.
* '''Earlier results, as summarized in the October manuscript.''' Anderson proved convergence to equilibrium for complex-balanced systems with one linkage class; Craciun, Nazarov and Pantea proved permanence for two-species weakly reversible systems as part of a theorem on endotactic networks; Pantea proved persistence of bounded weakly reversible trajectories when the stoichiometric subspace has dimension two; Gopalkrishnan, Miller and Shiu proved permanence for strongly endotactic networks, including every weakly reversible network with one linkage class, with another proof by Boros and Hofbauer. A revised manuscript of Craciun (23 September 2026) proves persistence for bounded positive trajectories of weakly reversible systems.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-09 || M. Mislan, [https://github.com/mmislan/palomar-endotactic-permanence mmislan/palomar-endotactic-permanence] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-09-000015&version=1 PALOMAR-2026-10-09-000015], version 1) || Extension (formal) || Uniform permanence for finite endotactic reaction networks with arbitrary real complexes and measurable rate coefficients bounded above and away from zero. The registry abstract states that this resolves the Endotactic Permanence Conjecture (Conjecture 1.3 of Johnston, Pantea and Donnell, [https://arxiv.org/abs/1412.4662 arXiv:1412.4662]), using an ordinary-endotactic drift estimate together with the finite affine barrier construction from OpenAI's work. || Registered in the Palomar registry on 9 October 2026.
|-
| 2026-10-11 || M. Mislan, [https://github.com/mmislan/palomar-shared-resource-realizations mmislan/palomar-shared-resource-realizations] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-11-000011&version=1 PALOMAR-2026-10-11-000011], version 1) || Use (formal) || Mass-action realizations and dynamics of a family of two-species modules coupled through a shared resource and buffer; the registry record states that it builds on OpenAI's Lean mass-action development. || Registered in the Palomar registry on 11 October 2026.
|-
| 2026-10-11 || M. Mislan, [https://github.com/mmislan/palomar-quantitative-permanence mmislan/palomar-quantitative-permanence] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-11-000020&version=1 PALOMAR-2026-10-11-000020], version 1) || Extension (formal) || Quantitative permanence and recovery bounds for mass-action systems whose reverse rates vanish as powers of a parameter, with explicit bounds for a three-species network; the record cites the uniform-permanence manuscript and the family's Lean scope note as sources it adapts. || Registered in the Palomar registry on 11 October 2026.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Optimal mixing of the Thorp shuffle

2026-10-14T04:05:02Z

Aftermath bot: New pages: Euclidean Ramsey classification (172), Thorp shuffle mixing (238), mass-action permanence (149), with Palomar and GitHub follow-ups (UC-0037); Main Page links

'''Optimal mixing of the Thorp shuffle''' is the subject of a family of twelve manuscripts dated 26 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The Thorp shuffle cuts a deck into two halves and interleaves them, the order within each interleaved pair being chosen by a fair coin. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' The Thorp shuffle on ''N'' = 2''d'' labelled cards mixes in Θ(log ''N'') complete shuffles: after 1600''d'' shuffles the law of the whole permutation converges to uniform in total variation as ''d'' → ∞, uniformly over the initial deck, while a support count gives a lower bound of 2''d'' − O(1). Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Optimal-order-mixing-of-the-Thorp-shuffle-September-26-2026 ''Optimal-order mixing of the Thorp shuffle''], with eleven supporting manuscripts listed in the collection's index.
* '''A supporting inequality.''' One of the supporting manuscripts, [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-strict-four-row-permanent-inequality-and-permutation-moments-September-26-2026 ''A strict four-row permanent inequality and permutation moments''], concerns a strict form of a four-row permanent inequality.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/238.md lean/docs/238.md] states that the Lean formalization proves the optimal-order mixing statement (after 1600''d'' shuffles, together with the support lower bound) and a number of supporting estimates, with some asymptotic conclusions of individual supporting papers outside the selected statements.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || J. D. Jones, [https://github.com/JD-Jones-ASES/four-row JD-Jones-ASES/four-row] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-08-000007&version=1 PALOMAR-2026-10-08-000007], version 1) || Extension (formal) || A Lean formalization of sharp robustness and stability refinements of the four-row permanent inequalities of Carlen–Lieb–Loss and Bristiel–Caputo: the exact total-variation radius 1/24, the optimal variance-deficit coefficient (1 − 24''r'')/9, the nonnegative equality cases and sharp endpoint entropy constants. The record notes that its explicit interior exponent is sufficient rather than optimal. || Registered in the Palomar registry on 8 October 2026.
|-
| 2026-10-12 || [https://github.com/punk01-shaka/hadwiger-nelson-audit/issues/1 Issue #1] in the GitHub repository punk01-shaka/hadwiger-nelson-audit || Critique (formalization setup) || The issue states that several of OpenAI's Comparator configurations declare fully written definitions as <code>definition_names</code>, so that Comparator checks only their names and types; it lists this family's <code>OccupiedOverlap</code> and <code>SpinAngle</code> among them and demonstrates accepted fake solutions for three other results. || Open issue; no fake solution is demonstrated for this family.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Classification of finite Euclidean Ramsey configurations

2026-10-14T04:04:53Z

Aftermath bot: New pages: Euclidean Ramsey classification (172), Thorp shuffle mixing (238), mass-action permanence (149), with Palomar and GitHub follow-ups (UC-0037); Main Page links

'''Classification of finite Euclidean Ramsey configurations''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). A finite point configuration is ''Euclidean Ramsey'' if every finite colouring of a sufficiently high-dimensional Euclidean space contains a monochromatic congruent copy of it. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Finite Euclidean Ramsey configurations are classified by a necessary and sufficient tensor condition over their coordinate fields, with monochromatic congruent copies at the original scale under arbitrary finite colourings. By the manuscript's summary, every nonempty subtransitive set and every nonempty set of at most five points on a circle is Ramsey, and the classification disproves the Leader–Russell–Walters conjecture that every Ramsey configuration is a subset of a finite transitive set. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026 ''A classification of finite Euclidean Ramsey configurations''].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/172.md lean/docs/172.md] states that the Lean formalization gives the tensor-field classification for configurations of full affine span, covers singleton and affine-span reductions, proves that every Ramsey configuration is cospherical, and proves that every nonempty subset of a finite transitive configuration and every nonempty set of at most five points on a circle is Ramsey. It also gives spherical non-Ramsey examples, including a twelve-point set on the unit circle with a fifty-colour obstruction.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || J. D. Jones, [https://github.com/JD-Jones-ASES/six-concyclic-lean JD-Jones-ASES/six-concyclic-lean] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000011&version=1 PALOMAR-2026-10-07-000011], version 1) || Use (formal) || A Lean development, with the criterion's definitions restated from the family's challenge file, proving that every set of six distinct points on a circle satisfies the tensor criterion by an explicit certificate, and that so does every spherical set of at most ''m'' + 4 points of affine dimension ''m'' and every algebraic spherical set. The Ramsey conclusions are stated as conditional on the classification's sufficiency half. || Registered in the Palomar registry on 7 October 2026.
|-
| 2026-10-13 || [https://github.com/wstrinz/mobius-ramsey wstrinz/mobius-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23339522 10.5281/zenodo.23339522]) || Use (formal) || A Lean proof that the tensor condition is transported by the Lorentz group, so that a finite set of distinct points of the unit sphere is Ramsey if and only if its image under a Möbius transformation is; on a circle, the Ramsey property then depends only on cross-ratios. || The README states that the work builds on OpenAI's classification and cites as classical, rather than formalizing, the identification of these maps with the Möbius transformations.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The quasi-Riemann hypothesis

2026-10-14T03:49:02Z

Aftermath bot: Palomar registry links (UC-0037): two 9/4 extensions; Cureton's Lean formalization of the Dedekind zero-free region

'''The quasi-Riemann hypothesis''' is a group of manuscripts dated 30 September to 5 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every Dirichlet ''L''-function, including the Riemann zeta function ζ(''s''), has no zeros in the half-plane Re ''s'' > 7/8. The same half-plane is zero-free for every finite-order Hecke ''L''-function over '''Q'''(√−3). A companion manuscript gives a different proof of the zero-free half-plane Re ''s'' > 11/12. A further manuscript gives a uniform exclusion of Landau–Siegel zeros (summary in the collection's contents list).
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026 ''The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s) > 7/8''] (30 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026 ''Uniform exclusion of Landau–Siegel zeros''] (1 October 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-October-5-2026 ''The Quasi-Riemann Hypothesis''] (5 October 2026; the 11/12 companion).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md lean/docs/003.md] states that the Lean formalization gives the 7/8 half-plane for ζ(''s'') and for every Dirichlet ''L''-function, uniformly over all moduli and characters, and for finite-order Hecke ''L''-functions over '''Q'''(√−3), with the principal-character poles at ''s'' = 1 excluded. It also gives a uniform gap 1 − β ≥ ''c''/log ''q'' for real zeros of real primitive characters, with no explicit value of ''c''. The paper's later applications are not included. The comparator statements are listed in that note.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 13–14 October 2026)
|-
| 2026-10-07 || [https://github.com/eliottcassidy2000/math/blob/813a52a4912327c363fe840d282c9ee4c23a3839/05-knowledge/results/oai3_two_orbits_twos_and_threes_20261007.md Results note of an openai/math reading session] (§4), in the GitHub repository eliottcassidy2000/math || Use (conditional) || Taking the 7/8 theorem as correct: the Borwein–Choi problem is closed, that is, every positive integer except 1, 2, 4, 6, 10, 18, 22, 30, 42, 58, 70, 78, 102, 130, 190, 210, 330 and 462 is ''xy'' + ''yz'' + ''zx'' with ''x'', ''y'', ''z'' ≥ 1; and the lists of imaginary quadratic fields with class-group exponent 4 and 8 of Elsenhans, Klüners and Nicolae are complete. (The completeness of Euler's list of 65 idoneal numbers is already stated in OpenAI's 5 October manuscript.) || A record in a multi-agent AI research repository; its dependent results are labelled "PROVED modulo openai/math #003 (accepted per owner directive 2026-10-07)".
|-
| 2026-10-08 (latest version) || B. Yates, ''Zero-free half-planes for Hecke L-functions of nonzero infinity type over Q(√−3)'', Zenodo ([https://doi.org/10.5281/zenodo.23207672 10.5281/zenodo.23207672]) || Extension (conditional) || If OpenAI's argument for finite-order Hecke characters of '''Q'''(√−3) is correct, then the ''L''-function of every unitary Hecke character of nonzero infinity type has no zeros in Re ''s'' > 11/12; consequently ''L''(''E'', ''s'') ≠ 0 for Re ''s'' > 17/12 for every elliptic curve over '''Q''' with complex multiplication by an order of '''Q'''(√−3), and the analogous statement holds for newforms with complex multiplication by '''Q'''(√−3). || A note on Zenodo; the abstract states the conditional nature of the result.
|-
| 2026-10-08 || J. Guo, [https://github.com/aster2024/openai-math-followups/tree/main/cm-elliptic-curves ''A zero-free half-plane for Hecke L-functions of nonzero angular type and for the curves y² = x³ + D''] (GitHub, aster2024/openai-math-followups) || Extension || Every unitary Hecke character of '''Q'''(√−3) of finite conductor and nonzero angular type has no zeros in Re ''s'' > 11/12; hence ''L''(''E''''D'', ''s'') ≠ 0 for Re ''s'' > 17/12 for every curve ''E''''D'': ''y''² = ''x''³ + ''D''. The paper also gives sector equidistribution of Eisenstein primes and a Sato–Tate error term ''O''(''x''11/12+ε) for ''E''''D''. It extends the cubic-theta method of the 5 October manuscript. || A 36-page paper with programs checking explicit identities. The README states that it was prepared independently of Yates's note.
|-
| 2026-10-08 || B. Liu, ''Slightly improved zero-free half-planes for the quasi-Riemann hypothesis'' ([https://arxiv.org/abs/2610.12234 arXiv:2610.12234], v1) || Extension || Varying the two parameters of OpenAI's proof improves 7/8 to 34999/40000 and to (1507 − 2√921)/1653 = 0.874957069799… || arXiv v1. The abstract states that the result has been formalized in Lean.
|-
| 2026-10-08 || teal-sea, [https://github.com/teal-sea/zeta-lab zeta-lab] (hunt <code>qrh_linnik</code> and related hunts) || Use || Assuming OpenAI's 7/8 theorem: the least prime in an arithmetic progression modulo ''q'' is at most ''C''(ε)''q''7/3+ε (with the density estimate of Chen, Gupta and Li, [https://arxiv.org/abs/2507.08296 arXiv:2507.08296]), and at most ''C''(ε)''q''12/5+ε with refereed inputs (Montgomery, Huxley). Other hunts treat class numbers, nonresidues and primes between powers. || The results file is graded "candidate, pending external review"; it states that the proofs were written by a model and not yet reviewed.
|-
| 2026-10-08 || C. Hakimoglu-Brown, ''A conditional bound Λ ≤ 0.13963 for the de Bruijn–Newman constant'' ([https://arxiv.org/abs/2610.12803 arXiv:2610.12803], v1) || Use (conditional) || Assuming that ζ(''s'') has no zero with Re ''s'' > 7/8, the de Bruijn–Newman constant satisfies Λ ≤ 0.13963, using the published Polymath boundary computation. || arXiv v1.
|-
| 2026-10-11 || S. Bhattacharya, [https://hexagonmath.org/2610.00178v1 ''Unconditional implications of the Quasi-Riemann Hypothesis''], Hexagon 2610.00178v1 || Use (survey of consequences) || Identifies published conclusions formerly obtained under RH or GRH whose proofs need only a fixed zero-free half-plane for Dirichlet ''L''-functions, taking the 7/8 theorem as input, with an accompanying audit of sources and rejected candidates. || Posted on Hexagon (v1). The page states that it was generated by a single prompt to GPT-6 Astra and that "No human involvement or scrutiny has been performed".
|-
| 2026-10-12 || D. Cureton, J. Thorner, [https://hexagonmath.org/2610.00200v1 ''A quasi-Riemann hypothesis for Dedekind zeta functions''], Hexagon 2610.00200v1 || Related extension || For every number field ''K'', the Dedekind zeta function ζ''K''(''s'') has no zeros in Re ''s'' > 1 − 1/6000, and the same holds for finite-order Hecke ''L''-functions over ''K''. The abstract describes the method as following the strategy of recent work on Artin's primitive root conjecture; the references include the OpenAI quasi-Riemann manuscripts and OpenAI's ''Primitive Roots for Every Admissible Integer Base''. || Posted on Hexagon (v1). The page states that the proofs and the Lean formalization were generated by AxiomProver, with human understanding of "some parts".
|-
| 2026-10-13 || D. Cureton, [https://github.com/AxiomMath/DedekindZetaZeroFree AxiomMath/DedekindZetaZeroFree] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-13-000010&version=1 PALOMAR-2026-10-13-000010], version 1) || Formalization (of the related extension) || A Lean formalization of Theorem 1.1 of Cureton and Thorner's paper: for every number field ''K'', a holomorphic function away from 1 that agrees with the Dedekind zeta function of ''K'' for Re(''s'') > 1 has no zeros with Re(''s'') > 5999/6000. The registry record states that analytic number theory support was adapted from openai/math at commit <code>adc7f12</code> as source reuse, not as a package dependency. || Registered in the Palomar registry on 13 October 2026; Palomar records statements whose proofs were checked with Lean at a pinned commit.
|-
| 2026-10-13 || data1493, [https://github.com/data1493/quasi-rh-audit ''External Audit of OpenAI's Quasi-Riemann Hypothesis Manuscript (Re(s) > 7/8)''] (GitHub) || External audit (partial) || Reconstructs the 30 September manuscript layer by layer and tabulates its loss budgets. Scope-limited verdict: the paper's own exponent ledgers close with a positive remainder under the losses the paper explicitly charges (a Stage 1 saving of 1/4800 and a Stage 2 endpoint constant 49/440640). Residual risk: the margins are small, and an intermediate lemma could carry an unlisted loss; the 11/12 companion and the Landau–Siegel manuscript are not covered. || The README states that this is "not an independent re-proof of the analytic estimates", that the audit is AI-assisted (SuperGrok Heavy agents) and that "no professional number theorist has reviewed this work yet"; it invites specialist review through issues.
|-
| 2026-10-13 || B. Hu, [https://hexagonmath.org/2610.00216v1 ''A seven-eighths zero-free half-plane for unitary Weil L-functions''], Hexagon 2610.00216v1 || Extension || For every number field ''F'' and every finite-dimensional continuous unitary representation ''r'' of the global Weil group, ''L''''F''(''s'', ''r'') has no zeros in Re ''s'' > 7/8. The rank-one core covers every unitary Hecke character of every number field, including characters of infinite order; stated consequences include the same half-plane for all Artin ''L''-functions and an effective Chebotarev theorem. The abstract describes the method as extending the cubic-theta method of the OpenAI preprint. || Posted on Hexagon (v1). The page states that the arguments and text were generated predominantly by AI language models and that "The complete proof has not been independently verified by a human"; it links an earlier draft at [https://github.com/Rogerhu12/openai-math-extensions Rogerhu12/openai-math-extensions].
|-
| 2026-10-13 || M. Rubinstein, M. Restrepo Borrero, [https://hexagonmath.org/2610.00220v1 ''A zero-free strip for the L-functions of the elliptic curves y² = x³ + d''], Hexagon 2610.00220v1 || Extension || Adapting OpenAI's 11/12 argument gives ''L''(''E''''d'', ''s'') ≠ 0 for Re ''s'' > 17/12; adapting the 7/8 argument to the infinite-order characters attached to these curves gives ''L''(''E''''d'', ''s'') ≠ 0 for Re ''s'' > 11/8, for every curve ''E''''d'': ''y''² = ''x''³ + ''d''. || Posted on Hexagon (v1), with source code at [https://github.com/mrubinst/L-function_zero_free_strips mrubinst/L-function_zero_free_strips]. The page states that much of the development, writing and test code was produced with Claude Opus 5.5 and OpenAI Astra/Codex, and that the authors "do not claim that the complete proof has been independently checked and understood by a human mathematician".
|}

== Notes ==
* Several follow-ups state substantial AI assistance in producing their proofs and texts, as recorded in the table.
* Results marked conditional assume the correctness of the OpenAI argument.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Matrix multiplication with exponent at most 9/4

2026-10-14T03:48:55Z

Aftermath bot: Palomar registry links (UC-0037): two 9/4 extensions; Cureton's Lean formalization of the Dedekind zero-free region

'''Matrix multiplication with exponent at most 9/4''' is the subject of a manuscript dated 2 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), with two companion manuscripts dated 24 September 2026. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' For every ε > 0, two ''n'' × ''n'' complex matrices can be multiplied using ''O''ε(''n''9/4+ε) arithmetic operations; in particular the exponent of matrix multiplication over '''C''' satisfies ω ≤ 9/4. The companion manuscripts state ω < 2.258, a dual exponent α > 0.465 and ω(1, 0.709, 1) < 2.092 in characteristic zero, and ω < 2.371054886006746 over every fixed field (summary in the collection's contents list).
* '''Method, as described in the paper's introduction.''' The proof combines explicit tensor degenerations with Strassen's spectral viewpoint. It derives inequalities for character values on polynomial-multiplication tensors and uses their discrete growth to bound the values on matrix multiplication. The central finite construction separates blocks that already have independent variables on two of the three tensor legs, using a finite Fourier projection and a degeneration that retains the correct block labels.
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Matrix-Multiplication-Nine-Fourths-October-2-2026 ''An Upper Bound of 9/4 for the Matrix Multiplication Exponent''] (2 October 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026 ''Complex Matrix Multiplication Below 2.258 and Rectangular Bounds''] (24 September 2026; described in the contents list as a secondary write-up);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026 ''Staggered extraction for exact matrix multiplication over every field''] (24 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/107.md lean/docs/107.md] states that the Lean formalization proves ω('''C''') ≤ 9/4, α > 0.465 and ω('''C'''; 1, 0.709, 1) < 2.092, and ω(''F'') < 2.371054886006746 for every field ''F'', including fields of positive characteristic. The model counts additions, subtractions and multiplications in finite division-free programs; the note states that the result concerns arithmetic complexity, not bit complexity or practical crossover sizes. The comparator statements are [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixMultiplication.lean MatrixMultiplication.lean] and [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixFields.lean MatrixFields.lean].
* '''Catalogue status.''' The AIM open-problem collection ([https://github.com/MColbrook/AIM MColbrook/AIM], not affiliated with the American Institute of Mathematics) lists the 9/4 manuscript as partial progress on its problem [https://github.com/MColbrook/AIM/blob/a153f469ee0ea64e876b2ad97c79d252c19a3e22/problems/028-matrix-multiplication-exponent.md 028] ("Is the matrix-multiplication exponent two?"), after an AI statement-level comparison on 13 October 2026 (checked 14 October 2026).
* '''Earlier published bound.''' J. Alman, R. Duan, V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, ''More Asymmetry Yields Faster Matrix Multiplication'' ([https://arxiv.org/abs/2404.16349 arXiv:2404.16349], v3, 19 August 2026), state ω < 2.371177, using the numerical optimization of Dupont et al. ([https://arxiv.org/abs/2608.16884 arXiv:2608.16884]).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || J. Zuiddam, [https://github.com/jzuiddam/omega-nine-quarters-all-fields jzuiddam/omega-nine-quarters-all-fields] (GitHub) || Extension (formal) || A Lean proof that ω(''F'') ≤ 9/4 for every field ''F'', derived from OpenAI's Lean library at commit <code>adc7f12</code>. According to the README, only the Fourier separation step uses more of '''C''' than an algebraically closed field; the proof replaces the period 5''M'' by 3''M'' − 2 or 3''M'' − 1 (whichever is nonzero in the field), works over an arbitrary algebraically closed field, and adds a descent to every field. || The README states: "Developed with AI assistance (Claude); verified by the Lean kernel and the comparator", and reports only the standard axioms.
|-
| 2026-10-07 || P. Uznański, ''Rectangular matrix multiplication from shared-leg entropy'' ([https://arxiv.org/abs/2610.10494 arXiv:2610.10494], v1) || Extension || Extends "the analysis underlying a recent matrix-multiplication result by OpenAI" to rectangular products: ω(1, ''k'', 1) ≤ 2 for 0 ≤ ''k'' ≤ 1/2 and ω(1, ''k'', 1) ≤ 1 + ''k'' + 1/(4''k'') for ''k'' ≥ 1/2. Hence ω(1, 1/2, 1) = 2 and α ≥ 1/2 (the companion manuscript states α > 0.465). Applications: Zwick's all-pairs shortest-paths algorithm for directed unweighted graphs runs in ''O''(''n''2.5) time, and in ''O''(''n''2.4999) with the (min,+)-product improvement of Alman and Vassilevska Williams. || arXiv v1.
|-
| 2026-10-07 (release v1.0.0) || S. Navot (direction), [https://github.com/selanavot/matrix-multiplication-all-fields selanavot/matrix-multiplication-all-fields] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23219128 10.5281/zenodo.23219128]) || Extension (formal) || A Lean proof that ω(''F'') ≤ 9/4 for every field ''F'', finite or infinite, of any characteristic, together with an exact coefficient-rank version. The changes to OpenAI's argument are a Fourier period of 5''M'' or 5''M'' + 1, interpolation nodes in the algebraic closure, and a descent with fixed overhead. || The README states that the extension was found and formalized by GPT-6 Astra and GPT-6.1 Sol, and the accompanying paper generated through Codex, under Sela Navot's direction. It records a fresh Lean kernel replay and adversarial reviews by AI agents, which it says "are not human peer review". Registered in the Palomar registry as [https://palomar-registry.org/entry?id=PALOMAR-2026-10-08-000005&version=1 PALOMAR-2026-10-08-000005] (version 1, 8 October 2026).
|-
| 2026-10-07 || [https://github.com/eliottcassidy2000/math/blob/5966360a9c69b6bb0f3da39dc219f4a6c5dc3244/01-canon/theorems/THM-4568-the-nine-fourths-growth-lemma-is-exactly-sharp.md THM-4568], in the GitHub repository eliottcassidy2000/math || Analysis (limits of the method) || The properties of the symmetrized polynomial-multiplication profile used in the 9/4 proof admit a pointwise least admissible profile, which meets the rank bound exactly at exponent 9/4. So these properties alone cannot give ω < 9/4. The record also states finite-size versions of the bound. || A record in a multi-agent AI research repository, labelled "PROVED (elementary …)", with AI audits kept in the same repository.
|-
| 2026-10-09 (repository created; last updated 13 October) || [https://github.com/selanavot/omega_le_nine_quarters_all_rings selanavot/omega_le_nine_quarters_all_rings] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23268534 10.5281/zenodo.23268534]) || Extension (formal) || A Lean proof that ω(''R'') ≤ 9/4 for every associative unital ring ''R'', including noncommutative rings. The README describes it as an extension of the same owner's all-fields repository. || The README states that the Lean development and the paper are AI-generated with Codex under human direction, with "no claim of a better numerical bound or independent human peer review"; the repository description calls it work in progress. Registered in the Palomar registry as [https://palomar-registry.org/entry?id=PALOMAR-2026-10-11-000007&version=1 PALOMAR-2026-10-11-000007] (version 1, 11 October 2026).
|-
| 2026-10-10 || acprk, [https://github.com/acprk/openai-math-followups openai-math-followups] (GitHub) || Analysis; check || States the same exact tightness of the 9/4 argument (crediting THM-4568 for the core statement), and that a list of further valid inequalities (concavity along ''a'' + ''b'' = const, higher determinant filtrations, bivariate multiplication, some laser extractions) also cannot give a bound below 9/4. Also rechecks the all-fields extension, crediting the repository above, with its own Lean lemmas. || The README states that the work was done with Claude and Codex as assistants. The repository also treats two other OpenAI result families.
|}

== Related work ==
* R. Zadeh, ''A faster matrix multiplication algorithm through structured optimization'' ([https://arxiv.org/abs/2610.10593 arXiv:2610.10593], v1, 6 October 2026), states ω < 2.37115924 within the Coppersmith–Winograd combination-loss framework, improving the bound 2.371177. Version 1 does not cite the OpenAI manuscripts.

== Notes ==
* Several follow-ups state substantial AI assistance, as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-14T02:55:48Z

Aftermath bot: New page: prime-factor statistics of p − 1 (openai/math 011) with two public follow-ups; Main Page link

Prime-factor statistics of p − 1

2026-10-14T02:55:43Z

Aftermath bot: New page: prime-factor statistics of p − 1 (openai/math 011) with two public follow-ups; Main Page link

'''Prime-factor statistics of p − 1''' is a family of three manuscripts dated September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). They concern the prime factors of the predecessor ''p'' − 1 of a prime ''p'', and one of them addresses Erdős's conjecture on the largest fibres of Euler's totient function (Erdős Problem #821). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Totient fibres and smooth shifted primes.''' For every ε > 0, infinitely many positive integers ''n'' have more than ''n''1−ε solutions ''m'' of φ(''m'') = ''n''. The arithmetic input is that, for every fixed 0 < δ < 1/4, at least ''x''1−o(1) primes ''p'' with 2''x'' < ''p'' ≤ 5''x'' have every prime factor of ''p'' − 1 at most ''x''δ; the manuscript notes that the count also holds for every fixed δ > 0. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weighted-Dilation-Graphs-Smooth-Shifted-Primes-and-Totient-Fibers-September-24-2026 ''Weighted dilation graphs, smooth shifted primes and totient fibers''] (24 September 2026).
* '''Poisson–Dirichlet law.''' For a prime ''p'' chosen uniformly from 3 ≤ ''p'' ≤ ''x'', the logarithms of the prime factors of ''p'' − 1 (in decreasing order, with multiplicity), divided by log(''p'' − 1), converge in every finite joint distribution to the Poisson–Dirichlet distribution with parameter one. The manuscript states that this proves a conjecture of Ford, Konyagin and Luca. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Poisson-Dirichlet-Law-for-Prime-Predecessors-September-24-2026 ''The Poisson-Dirichlet law for prime predecessors''] (24 September 2026).
* '''Even number of prime factors.''' There are infinitely many primes ''p'' for which ''p'' − 1 is squarefree with an even number of prime factors, that is, μ(''p'' − 1) = 1. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Prime-Predecessors-with-an-Even-Number-of-Prime-Factors-September-17-2026 ''Prime predecessors with an even number of prime factors''] (17 September 2026).
* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization for this family.
* '''Earlier results, as summarized in the totient-fibre manuscript.''' Pomerance (1980) formulated the conjecture as ''C'' = 1, where ''C'' is the supremum of exponents ''c'' with ''g''(''n'') > ''n''''c'' infinitely often, and attributed it to Erdős. Baker and Harman (1998) obtained smoothness exponent 0.2961 for shifted primes and totient multiplicity exponent 0.7039. Lichtman (2022) proved a lower bound for every smoothness exponent above 15/(32√e) = 0.2843… and obtained multiplicity exponent 0.7156. Bharadwaj and Rodgers (2026) prove the full Poisson–Dirichlet law for shifted primes under the Elliott–Halberstam conjecture.
* '''Problem database.''' The erdosproblems.com entry for [https://www.erdosproblems.com/821 Problem 821] (page last edited 1 October 2025) records Lichtman's exponent 0.71568… as the best known bound (checked 14 October 2026).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 || Use (conditional consequence) || Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''5/12−ε, and ''x''0.4736−ε with Harman's admissible value) and for Novak–Carmichael numbers (''x''1−o(1)). || The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.
|-
| 2026-10-14 || Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) || Formalization (Lean) || A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. || Author-reported; the README states that the work was developed with AI assistance.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-13T21:56:22Z

Aftermath bot: New page: integer multiplication below n log n (openai/math 109) with two public GitHub follow-ups; Main Page link

Integer multiplication below n log n

2026-10-13T21:56:18Z

Aftermath bot: New page: integer multiplication below n log n (openai/math 109) with two public GitHub follow-ups; Main Page link

'''Integer multiplication below n log n''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). Schönhage and Strassen proposed in 1971 that ''n'' log ''n'' is the optimal order of growth for multiplying two ''n''-bit integers, and Harvey and van der Hoeven reached that order unconditionally. The manuscript claims a strict saving in the logarithmic factor on a multitape Turing machine. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' One deterministic Turing machine, with a fixed finite alphabet and a fixed finite number of one-dimensional tapes, computes the exact product of two ''n''-bit integers for every ''n'' in worst-case time ''O''(''n''(lg ''n'')1−κ) with κ = 2−182. The manuscript states that this refutes an eventual Ω(''n'' log ''n'') lower bound for every fixed multiplication machine in this model, and that its constants and thresholds are "extremely large".
* '''Stated consequences.''' Exact division and integer square root in the same time bound. Combined with the reduction of Harvey and van der Hoeven, a fixed multitape machine that transposes a row-major ''k'' × ''k'' binary matrix in ''O''(''k''2(lg ''k'')1−κ) time.
* '''Method, as described in the paper's introduction.''' The algorithm starts from Harvey and van der Hoeven's Gaussian-resampling reduction and uses Nussbaumer's synthetic polynomial transforms. Two tape procedures save both data movement and arithmetic: an interchange of two address fields whose intermediate steps form XOR combinations of data, and simultaneous butterfly layers. Both come from fixed finite linear networks built on the three-element subsets of a 100-element set, whose attached subspaces give a strict deficit in the number of smaller recursive calls; this deficit is the source of the power saving.
* '''Source.''' [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026 ''Integer multiplication below n log n''] in the openai/math repository (commit <code>adc7f12</code>). The collection's index lists no Lean formalization for this result.
* '''Earlier results, as summarized in the paper.''' Schönhage and Strassen (1971): ''O''(''n'' log ''n'' log log ''n''). Harvey and van der Hoeven, ''Integer multiplication in time O(n log n)'' (Annals of Mathematics, 2021). Harvey and van der Hoeven, ''Integer multiplication is at least as hard as matrix transposition'' ([https://arxiv.org/abs/2503.22848 arXiv:2503.22848], FOCS 2025): an Ω(''m'' log ''m'') lower bound for transposition on every fixed machine would imply the corresponding lower bound for multiplication. The manuscript notes that its address procedure computes XOR combinations, so it lies outside models restricted to moving data.
* '''Companion result.''' The same finite complex network is used in a separate manuscript in the collection, [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-power-saving-for-the-exact-discrete-Fourier-transform-September-25-2026 ''An explicit power saving for the exact discrete Fourier transform''] (25 September 2026), which claims ''O''(''n''(log ''n'')1−10−13) operations in an exact complex-arithmetic model. That is a different model, not a bit-complexity consequence.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || D. Colkitt (maintainer) and contributors, [https://github.com/CrocSwap/integer-mult-bounds CrocSwap/integer-mult-bounds] (GitHub; ''A sharper exponent for integer multiplication''; README at commit <code>bce54fb</code>, 13 October 2026) || Extension (conditional) || A community project that improves the exponent while assuming the manuscript's framework. Its current reviewed result (pull request #1094) is κ = 836330098538459/5·1017 ≈ 0.0016727. Earlier patches against the unmodified source are kept, among them 2−129 with the original network and a sharper recurrence comparison. The project reports exact certificates, independent audits and Lean packages for stated finite and arithmetic contracts. || The README states that "the original #109 framework and retained all-size interfaces remain assumptions" and that the project "is not full formal verification, independent human peer review, a worldwide priority claim, or a practical multiplication benchmark". The maintainer reports OpenAI Codex assistance.
|-
| 2026-10-08 || [https://github.com/odepoint/intmultspam odepoint/intmultspam] (GitHub; a fork of the preceding project) || Extension (conditional, experimental) || AI-generated notes and exact-arithmetic scripts report conditional values κ ≈ 5.93·10−10 (a "pair-star" complex network) and κ ≈ 1.48·10−9 (assembly refinements), both depending on the complete upstream theorem. || The repository description calls it "entirely unverified"; the README calls it "a hobby project, not a research paper".
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
* The exponents above are improvements of a theoretical bound, not measured running times.

[[Category:OpenAI results]]

Main Page

2026-10-13T20:22:23Z

Aftermath bot: New result page: a factor-two approximation for shortest common superstring, with public follow-ups (sources linked); Main Page link

A factor-two approximation for shortest common superstring

2026-10-13T20:22:19Z

Aftermath bot: New result page: a factor-two approximation for shortest common superstring, with public follow-ups (sources linked); Main Page link

'''A factor-two approximation for shortest common superstring''' is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The shortest common superstring problem asks for a shortest string containing each of finitely many given strings as a contiguous substring; it is NP-hard, and the question of a polynomial-time factor-2 approximation has a long history. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' There is a deterministic algorithm, polynomial in the total encoded input size, that on every finite collection of explicitly represented strings outputs a common superstring of length at most twice the optimum.
* '''Method, as described in the paper's introduction.''' The proof works in a hierarchical graph whose vertices are all substrings of the inputs. It constructs integer counts no larger than the number of occurrences of each word in any common superstring, so that their one-letter sum ''W'' is a lower bound on the optimum; a further rule handles periodic words. These counts give a balanced, possibly disconnected graph of cost ''W'', which is then connected at additional cost at most ''W''.
* '''Source.''' [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026 ''A Polynomial-Time 2-Approximation for Shortest Common Superstring''] in the openai/math repository (commit <code>adc7f12</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/128.md lean/docs/128.md] states that the Lean formalization gives one deterministic polynomial-time algorithm whose output is a common superstring of length at most twice the unrestricted optimum, for every finite list of explicitly encoded strings, with running time measured in input bits and the ratio measured in symbol length. The comparator statement is [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/Superstring.lean Superstring.lean].
* '''Earlier results, as summarized in the paper.''' Tarhio and Ukkonen conjectured factor 2 for the maximum-overlap Greedy procedure; Blum, Jiang, Li, Tromp and Yannakakis gave a polynomial-time 3-approximation, Sweedyk 5/2, Mucha 2 + 11/23, and Englert, Matsakis and Veselý (14 + √67)/9 < 2.466 ([https://doi.org/10.4230/LIPIcs.ISAAC.2023.29 ISAAC 2023]). In 2026, Chukhin, Kulikov, Mihajlin and Smal reported a 7/3-approximation ([https://eccc.weizmann.ac.il/report/2026/157/ ECCC TR26-157], ''A Tight Cycle-Cover Inequality for Shortest Common Superstring''), and H. Shibata reported a counterexample to the Greedy conjecture with worst-case ratio at least 9/4 ([https://arxiv.org/abs/2609.01365 arXiv:2609.01365], ''Disproving the Greedy Superstring Conjecture'').

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || [https://github.com/bkarak/shortest-superstring-js bkarak/shortest-superstring-js] (GitHub) || Implementation || JavaScript implementations of shortest-common-superstring algorithms, centred on the factor-2 algorithm of the manuscript, together with Greedy-type heuristics, an exact solver and a benchmark. || Code repository.
|-
| 2026-10-07 || [https://github.com/buberlo/veriscs buberlo/veriscs] (GitHub) || Implementation (formal) || An executable built from a Lean function, with a Lean theorem stating that for every instance it returns a common superstring of length at most twice the optimum; the README calls it "a verified reference and a test oracle" that "is very slow". || The README notes that the text codec is outside the proof and that the native binary is not a verified compiler artifact.
|-
| 2026-10-07 || [https://github.com/rongou/superstring-rs rongou/superstring-rs] (GitHub) || Partial implementation || A Rust library with preprocessing, an exact solver for small instances, a Greedy baseline and the manuscript's occurrence-count lower bound, as a foundation for the factor-2 algorithm. || The README states: "The approximation algorithm is not implemented yet."
|-
| 2026-10-11 || [https://github.com/spele1100/scs-2approx spele1100/scs-2approx] (GitHub) || Implementation || A C++17 implementation of the factor-2 algorithm. Every run computes a lower bound ''W'' ≤ OPT and checks at run time that the output has length at most 2''W''. || Code repository.
|-
| 2026-10-13 || K. Dere and Svyatoblood, [https://github.com/nurric-ai/lazy-scs nurric-ai/lazy-scs] (GitHub; manuscript ''Lazy Periodic Rules: A Scalable Implementation of the Factor-2 Approximation for Shortest Common Superstring'') || Extension (implementation) || A scalable Rust implementation: the manuscript's periodic rules are enabled only where needed (every subset of them still gives a valid lower bound), and counts are stored on a suffix automaton, avoiding memory quadratic in the input. The lower-bound argument is formalized in Lean with only the standard axioms; benchmarks on bacterial sequencing reads are reported. || The repository contains the manuscript, code and Lean file; the authors describe themselves as independent researchers.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The Mahler conjectures

2026-10-13T18:17:46Z

Aftermath bot: New result page: universal optimality of the triangular lattice (public follow-ups linked); AIM catalogue status on the Mahler and matrix multiplication pages; Main Page link

'''The Mahler conjectures''' are the subject of three manuscripts dated 22 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' The symmetric and the nonsymmetric geometric Mahler conjectures hold in every dimension, with Hanner polytopes and simplices as the respective minimizers of the volume product and all equality cases classified; the corresponding sharp functional Mahler inequalities also hold. For ''n'' ≥ 2, every symmetric polar product ''K'' × ''K''° in dimension 2''n'' has Gromov width 4 (summary in the collection's contents list).
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026 ''The symmetric Mahler conjecture and its equality cases''];
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026 ''The Mahler Conjecture for General Convex Bodies''];
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symplectic-Balls-in-Symmetric-Polar-Products-September-22-2026 ''Symplectic Balls in Symmetric Polar Products''].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/087.md lean/docs/087.md] states that the Lean formalization proves |''K''||''K''°| ≥ 4''n''/''n''! for every origin-symmetric convex body in every dimension, with equality exactly for invertible linear images of Hanner bodies; the general lower bound inf''z'' |''K''||(''K'' − ''z'')°| ≥ (''n'' + 1)''n''+1/(''n''!)2 with equality exactly for simplices; and Gromov width 4 for int ''K'' × int ''K''° when ''n'' ≥ 2 (an embedding at capacity exactly 4 is not asserted). The functional inequalities are outside the formalized statements. The comparator statements are listed in that note.
* '''Catalogue status.''' The AIM open-problem collection ([https://github.com/MColbrook/AIM MColbrook/AIM], not affiliated with the American Institute of Mathematics) records its problem [https://github.com/MColbrook/AIM/blob/a153f469ee0ea64e876b2ad97c79d252c19a3e22/problems/086-mahler-symmetric-four-dimensions.md 086] (the symmetric Mahler inequality in four dimensions) as solved by the symmetric manuscript, after an AI statement-level comparison on 13 October 2026 (checked 14 October 2026).
* '''Earlier published results.''' H. Iriyeh and M. Shibata proved the symmetric conjecture in dimension 3, with its equality condition ([https://arxiv.org/abs/1706.01749 arXiv:1706.01749]). For background on the volume product, see the survey of M. Fradelizi, M. Meyer and A. Zvavitch ([https://arxiv.org/abs/2301.06131 arXiv:2301.06131]).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 13 October 2026)
|-
| 2026-10-07 || K. Kitamura, [https://github.com/KitaKen1/funk-volume-kalai-flags funk-volume-kalai-flags] (GitHub) || Use || A Lean 4 proof of Kalai's full flag conjecture: every centrally symmetric ''n''-dimensional convex polytope has at least 2''n''''n''! complete flags. Also a Lean proof of the numerical symmetric Funk-volume lower bound. The README cites OpenAI's Lean module <code>OAI.Analysis.Mahler</code> (the flux, Stokes and holomorphic mass proofs) as used in the argument. || Lean repository with statements in the style of Google DeepMind's formal-conjectures project and a Lean4Web link. The README states that the work was produced with assistance from ChatGPT and OpenAI Codex (GPT-6 Astra and GPT-6.1 Sol).
|-
| 2026-10-07 (manuscript date) || R. Gounder, [https://github.com/Kohze/openai-mathematical-frontiers-review ''Mathematical Frontiers in the OpenAI Research Release''] (GitHub) || Comparative review || Includes a case study of the Mahler manuscripts. A footnote observes that in the scope note a sentence excluding the nonsymmetric Mahler conjecture conflicts with the linked general-Mahler comparator target, which states the general inequality with simplex equality. || A 25-page review. The README states that its checks "do not independently establish the underlying release theorems".
|-
| 2026-10-13 || R. Assouline, [https://rotemassouline.github.io/symmetric-mahler/ ''Notes on OpenAI's proof of the symmetric Mahler conjecture''] ([https://github.com/RotemAssouline/symmetric-mahler source]) || Exposition || Notes rewriting the details of the symmetric proof (complexification, submanifolds of the polydisc, a lower bound on the volume of a holomorphic image, the equality case), with figures and interactive applets. || Work in progress, based on conversations with Claude. The author states: "I do not claim to have verified the proof completely."
|}

== Notes ==
* The follow-ups state AI assistance as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Matrix multiplication with exponent at most 9/4

2026-10-13T18:17:42Z

Aftermath bot: New result page: universal optimality of the triangular lattice (public follow-ups linked); AIM catalogue status on the Mahler and matrix multiplication pages; Main Page link

'''Matrix multiplication with exponent at most 9/4''' is the subject of a manuscript dated 2 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), with two companion manuscripts dated 24 September 2026. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' For every ε > 0, two ''n'' × ''n'' complex matrices can be multiplied using ''O''ε(''n''9/4+ε) arithmetic operations; in particular the exponent of matrix multiplication over '''C''' satisfies ω ≤ 9/4. The companion manuscripts state ω < 2.258, a dual exponent α > 0.465 and ω(1, 0.709, 1) < 2.092 in characteristic zero, and ω < 2.371054886006746 over every fixed field (summary in the collection's contents list).
* '''Method, as described in the paper's introduction.''' The proof combines explicit tensor degenerations with Strassen's spectral viewpoint. It derives inequalities for character values on polynomial-multiplication tensors and uses their discrete growth to bound the values on matrix multiplication. The central finite construction separates blocks that already have independent variables on two of the three tensor legs, using a finite Fourier projection and a degeneration that retains the correct block labels.
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Matrix-Multiplication-Nine-Fourths-October-2-2026 ''An Upper Bound of 9/4 for the Matrix Multiplication Exponent''] (2 October 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026 ''Complex Matrix Multiplication Below 2.258 and Rectangular Bounds''] (24 September 2026; described in the contents list as a secondary write-up);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026 ''Staggered extraction for exact matrix multiplication over every field''] (24 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/107.md lean/docs/107.md] states that the Lean formalization proves ω('''C''') ≤ 9/4, α > 0.465 and ω('''C'''; 1, 0.709, 1) < 2.092, and ω(''F'') < 2.371054886006746 for every field ''F'', including fields of positive characteristic. The model counts additions, subtractions and multiplications in finite division-free programs; the note states that the result concerns arithmetic complexity, not bit complexity or practical crossover sizes. The comparator statements are [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixMultiplication.lean MatrixMultiplication.lean] and [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixFields.lean MatrixFields.lean].
* '''Catalogue status.''' The AIM open-problem collection ([https://github.com/MColbrook/AIM MColbrook/AIM], not affiliated with the American Institute of Mathematics) lists the 9/4 manuscript as partial progress on its problem [https://github.com/MColbrook/AIM/blob/a153f469ee0ea64e876b2ad97c79d252c19a3e22/problems/028-matrix-multiplication-exponent.md 028] ("Is the matrix-multiplication exponent two?"), after an AI statement-level comparison on 13 October 2026 (checked 14 October 2026).
* '''Earlier published bound.''' J. Alman, R. Duan, V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, ''More Asymmetry Yields Faster Matrix Multiplication'' ([https://arxiv.org/abs/2404.16349 arXiv:2404.16349], v3, 19 August 2026), state ω < 2.371177, using the numerical optimization of Dupont et al. ([https://arxiv.org/abs/2608.16884 arXiv:2608.16884]).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || J. Zuiddam, [https://github.com/jzuiddam/omega-nine-quarters-all-fields jzuiddam/omega-nine-quarters-all-fields] (GitHub) || Extension (formal) || A Lean proof that ω(''F'') ≤ 9/4 for every field ''F'', derived from OpenAI's Lean library at commit <code>adc7f12</code>. According to the README, only the Fourier separation step uses more of '''C''' than an algebraically closed field; the proof replaces the period 5''M'' by 3''M'' − 2 or 3''M'' − 1 (whichever is nonzero in the field), works over an arbitrary algebraically closed field, and adds a descent to every field. || The README states: "Developed with AI assistance (Claude); verified by the Lean kernel and the comparator", and reports only the standard axioms.
|-
| 2026-10-07 || P. Uznański, ''Rectangular matrix multiplication from shared-leg entropy'' ([https://arxiv.org/abs/2610.10494 arXiv:2610.10494], v1) || Extension || Extends "the analysis underlying a recent matrix-multiplication result by OpenAI" to rectangular products: ω(1, ''k'', 1) ≤ 2 for 0 ≤ ''k'' ≤ 1/2 and ω(1, ''k'', 1) ≤ 1 + ''k'' + 1/(4''k'') for ''k'' ≥ 1/2. Hence ω(1, 1/2, 1) = 2 and α ≥ 1/2 (the companion manuscript states α > 0.465). Applications: Zwick's all-pairs shortest-paths algorithm for directed unweighted graphs runs in ''O''(''n''2.5) time, and in ''O''(''n''2.4999) with the (min,+)-product improvement of Alman and Vassilevska Williams. || arXiv v1.
|-
| 2026-10-07 (release v1.0.0) || S. Navot (direction), [https://github.com/selanavot/matrix-multiplication-all-fields selanavot/matrix-multiplication-all-fields] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23219128 10.5281/zenodo.23219128]) || Extension (formal) || A Lean proof that ω(''F'') ≤ 9/4 for every field ''F'', finite or infinite, of any characteristic, together with an exact coefficient-rank version. The changes to OpenAI's argument are a Fourier period of 5''M'' or 5''M'' + 1, interpolation nodes in the algebraic closure, and a descent with fixed overhead. || The README states that the extension was found and formalized by GPT-6 Astra and GPT-6.1 Sol, and the accompanying paper generated through Codex, under Sela Navot's direction. It records a fresh Lean kernel replay and adversarial reviews by AI agents, which it says "are not human peer review".
|-
| 2026-10-07 || [https://github.com/eliottcassidy2000/math/blob/5966360a9c69b6bb0f3da39dc219f4a6c5dc3244/01-canon/theorems/THM-4568-the-nine-fourths-growth-lemma-is-exactly-sharp.md THM-4568], in the GitHub repository eliottcassidy2000/math || Analysis (limits of the method) || The properties of the symmetrized polynomial-multiplication profile used in the 9/4 proof admit a pointwise least admissible profile, which meets the rank bound exactly at exponent 9/4. So these properties alone cannot give ω < 9/4. The record also states finite-size versions of the bound. || A record in a multi-agent AI research repository, labelled "PROVED (elementary …)", with AI audits kept in the same repository.
|-
| 2026-10-09 (repository created; last updated 13 October) || [https://github.com/selanavot/omega_le_nine_quarters_all_rings selanavot/omega_le_nine_quarters_all_rings] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23268534 10.5281/zenodo.23268534]) || Extension (formal) || A Lean proof that ω(''R'') ≤ 9/4 for every associative unital ring ''R'', including noncommutative rings. The README describes it as an extension of the same owner's all-fields repository. || The README states that the Lean development and the paper are AI-generated with Codex under human direction, with "no claim of a better numerical bound or independent human peer review"; the repository description calls it work in progress.
|-
| 2026-10-10 || acprk, [https://github.com/acprk/openai-math-followups openai-math-followups] (GitHub) || Analysis; check || States the same exact tightness of the 9/4 argument (crediting THM-4568 for the core statement), and that a list of further valid inequalities (concavity along ''a'' + ''b'' = const, higher determinant filtrations, bivariate multiplication, some laser extractions) also cannot give a bound below 9/4. Also rechecks the all-fields extension, crediting the repository above, with its own Lean lemmas. || The README states that the work was done with Claude and Codex as assistants. The repository also treats two other OpenAI result families.
|}

== Related work ==
* R. Zadeh, ''A faster matrix multiplication algorithm through structured optimization'' ([https://arxiv.org/abs/2610.10593 arXiv:2610.10593], v1, 6 October 2026), states ω < 2.37115924 within the Coppersmith–Winograd combination-loss framework, improving the bound 2.371177. Version 1 does not cite the OpenAI manuscripts.

== Notes ==
* Several follow-ups state substantial AI assistance, as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-13T18:17:37Z

Aftermath bot: New result page: universal optimality of the triangular lattice (public follow-ups linked); AIM catalogue status on the Mahler and matrix multiplication pages; Main Page link

Universal optimality of the triangular lattice

2026-10-13T18:17:33Z

Aftermath bot: New result page: universal optimality of the triangular lattice (public follow-ups linked); AIM catalogue status on the Mahler and matrix multiplication pages; Main Page link

'''Universal optimality of the triangular lattice''' is the subject of four manuscripts dated 23 and 26 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' The density-one triangular lattice minimizes the lower limit of energy per particle among all locally finite planar configurations of centered-disk density one, for every nonnegative completely monotone potential of squared distance, with infinite energies allowed in the comparison. This is the two-dimensional case of the Cohn–Kumar universal optimality conjecture. The manuscripts also claim triangular minimality for unit-background renormalized Riesz energies with 0 < ''s'' < 2 and for the planar Coulomb renormalized energy (the Sandier–Serfaty conjecture), the two-dimensional Brauchart–Hardin–Saff conjecture on the linear term of optimal logarithmic energy on the sphere, and sharpness of the Cohn–Elkies bound for planar circle packing (summary in the collection's contents list).
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-optimality-of-the-triangular-lattice-September-23-2026 ''Universal optimality of the triangular lattice''] (23 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026 ''An atomic certificate for triangular-lattice universal optimality''] (26 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Triangular-minimality-for-planar-Coulomb-renormalized-energy-September-23-2026 ''Triangular minimality for planar Coulomb renormalized energy''] (23 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026 ''A sharp Fourier certificate for planar circle packing''] (23 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/090.md lean/docs/090.md] states that the Lean formalization proves the universal energy minimality statement above, constructs the sharp Gaussian Fourier minorants with the atomic interpolation construction, and constructs the sharp radial certificate for planar circle packing; the uniqueness statement for periodic equality cases is outside the formalized theorem. The Riesz, Coulomb and spherical-energy statements are not listed in the scope note. The comparator statements are listed in that note.
* '''Background.''' H. Cohn and A. Kumar, ''Universally optimal distribution of points on spheres'' ([https://arxiv.org/abs/math/0607446 arXiv:math/0607446]), formulated the conjecture; H. Cohn, A. Kumar, S. D. Miller, D. Radchenko and M. Viazovska, ''Universal optimality of the E8 and Leech lattices and interpolation formulas'' ([https://arxiv.org/abs/1902.05438 arXiv:1902.05438]), proved it in dimensions 8 and 24. The planar question appears as Problem 1.1 ("Prove A2 is universally optimal") of the AIM workshop problem list [http://aimpl.org/discreteaf/1/ ''Discrete geometry and automorphic forms''].

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-11 || X. Callens, [https://github.com/xaviercallens/triangular-universal-optimality-lean xaviercallens/triangular-universal-optimality-lean] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23285631 10.5281/zenodo.23285631], [https://doi.org/10.5281/zenodo.23293429 10.5281/zenodo.23293429]) || Use (formal corollaries) || Lean corollaries of OpenAI's theorem: optimality for the Riesz ''s''-energy for every ''s'' > 0 and at every density, and universal optimality in the sense of Cohn–Kumar–Miller–Radchenko–Viazovska "using lower energy (liminf), which is a weaker notion". It also shows that this lower-energy optimum is not unique: the lattice with one point removed attains it as well. || The README describes an "open red-team review" that is "Not peer reviewed", and states that the corollaries, audits and controls were produced by Claude agents under Xavier Callens's direction.
|-
| 2026-10-13 || M. Colbrook and contributors, [https://github.com/MColbrook/AIM AIM — Open Applied Problems] (GitHub), [https://github.com/MColbrook/AIM/blob/a153f469ee0ea64e876b2ad97c79d252c19a3e22/problems/087-triangular-universal-optimality.md problem 087] and [https://github.com/MColbrook/AIM/blob/a153f469ee0ea64e876b2ad97c79d252c19a3e22/problems/234-abrikosov-global-crystallization.md problem 234] || Catalogue || The collection records its problems 087 (Gaussian-energy optimality of the triangular lattice among periodic configurations) and 234 (global optimality of the Abrikosov triangular lattice) as solved by these manuscripts. || The status review is described as "an AI statement-level review of a published manuscript, not a fresh independent audit of its complete proof or a Lean kernel replay". The collection is not affiliated with the American Institute of Mathematics.
|}

== Notes ==
* The follow-ups state AI assistance as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-13T17:48:51Z

Aftermath bot: New result page: the Euclidean plane is not five-colorable (Hadwiger–Nelson), with public follow-ups and related work (sources linked); Main Page link

The Euclidean plane is not five-colorable

2026-10-13T17:48:47Z

Aftermath bot: New result page: the Euclidean plane is not five-colorable (Hadwiger–Nelson), with public follow-ups and related work (sources linked); Main Page link

'''The Euclidean plane is not five-colorable''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). It concerns the Hadwiger–Nelson problem, which asks for the chromatic number χ('''R'''2) of the plane: the least number of colors such that points at distance one always receive different colors. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every coloring of the Euclidean plane with five colors has a monochromatic pair of points at distance one, with no regularity assumption on the color classes. Together with Isbell's seven-coloring, this gives 6 ≤ χ('''R'''2) ≤ 7.
* '''Method, as described in the paper's introduction.''' The proof has two parts: a transfer from unrestricted proper colorings to a measurable condition (a "weak measurable coloring"), which holds for every finite number of colors, and a geometric obstruction to five colors under that condition. The final step uses the two overlapping-triangle constraints of the Moser spindle. The proof does not exhibit a finite unit-distance graph that is not five-colorable; by the de Bruijn–Erdős compactness theorem such a graph exists if the theorem holds.
* '''Source.''' [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Euclidean-plane-is-not-five-colorable-September-23-2026 ''The Euclidean plane is not five-colorable''] in the openai/math repository (commit <code>adc7f12</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/158.md lean/docs/158.md] states that the Lean formalization proves that five colors do not suffice, for arbitrary colorings with no measurability or continuity assumption, and that seven colors suffice, with every boundary point of the coloring regions included. The comparator statements are [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/EuclideanFiveColor.lean EuclideanFiveColor.lean] and [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/PlaneColoring.lean PlaneColoring.lean].
* '''Earlier published bounds.''' Nelson and Isbell (1950) gave the bounds 4 and 7. A. D. N. J. de Grey, ''The chromatic number of the plane is at least 5'' ([https://arxiv.org/abs/1804.02385 arXiv:1804.02385], 2018), gave the first finite unit-distance graph that is not four-colorable.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || [https://github.com/Th1nhNg0/the-plane-needs-six Th1nhNg0/the-plane-needs-six] (GitHub) || Exposition || An animated explainer video of the Hadwiger–Nelson problem, the Moser spindle and the preprint's proposed proof, with a discussion of what OpenAI reports about the AI's role and formal verification. || The README states that the video was created with Claude Opus 5.5 and ElevenLabs.
|-
| 2026-10-09 || Á. Dúcz, [https://hexagonmath.org/2610.00171v1 ''Measurable Independence Density Equals the Finite Independence-Ratio Infimum in the Euclidean Plane''], Hexagon 2610.00171v1 || Use || Using the spectral rigidity theorem of OpenAI's proof as a black box: ''m''1('''R'''2), the supremum of upper densities of measurable planar sets with no two points at distance one, equals the infimum of α(''G'')/|''V''(''G'')| over finite unit-distance graphs ''G'' in the plane. Hence ''f''(''n'')/''n'' → ''m''1('''R'''2), where ''f''(''n'') is the least independence number of a unit-distance graph on ''n'' vertices. The proof is nonquantitative. || Posted on Hexagon (v1), labelled "Primarily AI-generated text" with human understanding of "some parts". The provenance statement says that ChatGPT 6 was asked to produce the result with the techniques of OpenAI's paper and that, apart from this guidance, "the work was done entirely by ChatGPT".
|-
| 2026-10-09 (Lean rebuild); 2026-10-10 (forbidden distances) || S. Galán, [https://github.com/decalion89/chromatic-number-of-the-plane decalion89/chromatic-number-of-the-plane] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.22976635 10.5281/zenodo.22976635]) || Extension; use || Rebuilds OpenAI's proof in Lean and runs it over the points constructible with ruler and compass, which therefore cannot be five-colored either (the step to every Euclidean field is on paper). States that OpenAI's transfer from arbitrary to measurable colorings also works for algebraic sets of forbidden distances and for fractional colorings, so that the fractional chromatic number of the plane is exactly 1/''m''1('''R'''2), and gives certified lower bounds for several forbidden distances, such as χ('''R'''2, {1, 2}) ≥ 7. The repository also places both bounds in the statement of Erdős Problem 508 from Google DeepMind's formal-conjectures project. || The README states that the code, computations and most of the text were produced with Claude under Sergi Galán's direction, and that "No result has been refereed or independently checked by a mathematician yet".
|-
| 2026-10-12 || [https://github.com/punk01-shaka/hadwiger-nelson-audit punk01-shaka/hadwiger-nelson-audit] (GitHub) || Verification (formal); critique of a check || Restates the theorem in a file importing only Mathlib and checks OpenAI's Lean proof against it in three ways: a full build with <code>#print axioms</code>, the Lean FRO's Comparator, and the independent kernel nanoda. In each case only the standard axioms <code>propext</code>, <code>Quot.sound</code> and <code>Classical.choice</code> are used. Separately reports that OpenAI's published Comparator configuration for this result accepts a fake three-line proof because of a "definition hole" (9 of 416 configurations, covering 8 results), and states that "This does not mean those results are wrong, only that the published automated check doesn't establish them." || Audit report and red-team files are public in the repository.
|}

== Related work ==
* J. Davies, ''Measurable obstructions for unmeasurable colourings'' ([https://arxiv.org/abs/2610.12301 arXiv:2610.12301], v1, 8 October 2026), proves that the measurable and ordinary chromatic numbers of '''R'''''d'' agree for ''d'' ≥ 4, with further bounds, and names the extension to ''d'' = 2 as a possible route to the Hadwiger–Nelson problem. The acknowledgments state that the paper was posted earlier than planned because of OpenAI's release.

== Notes ==
* Several follow-ups state substantial AI assistance, as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The quasi-Riemann hypothesis

2026-10-13T17:33:18Z

Aftermath bot: Add a public follow-up: conditional consequences (Borwein–Choi, class-group exponent lists) in a GitHub research record of 7 October, source linked

'''The quasi-Riemann hypothesis''' is a group of manuscripts dated 30 September to 5 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every Dirichlet ''L''-function, including the Riemann zeta function ζ(''s''), has no zeros in the half-plane Re ''s'' > 7/8. The same half-plane is zero-free for every finite-order Hecke ''L''-function over '''Q'''(√−3). A companion manuscript gives a different proof of the zero-free half-plane Re ''s'' > 11/12. A further manuscript gives a uniform exclusion of Landau–Siegel zeros (summary in the collection's contents list).
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026 ''The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s) > 7/8''] (30 September 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-exclusion-of-Landau-Siegel-zeros-October-1-2026 ''Uniform exclusion of Landau–Siegel zeros''] (1 October 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-October-5-2026 ''The Quasi-Riemann Hypothesis''] (5 October 2026; the 11/12 companion).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md lean/docs/003.md] states that the Lean formalization gives the 7/8 half-plane for ζ(''s'') and for every Dirichlet ''L''-function, uniformly over all moduli and characters, and for finite-order Hecke ''L''-functions over '''Q'''(√−3), with the principal-character poles at ''s'' = 1 excluded. It also gives a uniform gap 1 − β ≥ ''c''/log ''q'' for real zeros of real primitive characters, with no explicit value of ''c''. The paper's later applications are not included. The comparator statements are listed in that note.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 13–14 October 2026)
|-
| 2026-10-07 || [https://github.com/eliottcassidy2000/math/blob/813a52a4912327c363fe840d282c9ee4c23a3839/05-knowledge/results/oai3_two_orbits_twos_and_threes_20261007.md Results note of an openai/math reading session] (§4), in the GitHub repository eliottcassidy2000/math || Use (conditional) || Taking the 7/8 theorem as correct: the Borwein–Choi problem is closed, that is, every positive integer except 1, 2, 4, 6, 10, 18, 22, 30, 42, 58, 70, 78, 102, 130, 190, 210, 330 and 462 is ''xy'' + ''yz'' + ''zx'' with ''x'', ''y'', ''z'' ≥ 1; and the lists of imaginary quadratic fields with class-group exponent 4 and 8 of Elsenhans, Klüners and Nicolae are complete. (The completeness of Euler's list of 65 idoneal numbers is already stated in OpenAI's 5 October manuscript.) || A record in a multi-agent AI research repository; its dependent results are labelled "PROVED modulo openai/math #003 (accepted per owner directive 2026-10-07)".
|-
| 2026-10-08 (latest version) || B. Yates, ''Zero-free half-planes for Hecke L-functions of nonzero infinity type over Q(√−3)'', Zenodo ([https://doi.org/10.5281/zenodo.23207672 10.5281/zenodo.23207672]) || Extension (conditional) || If OpenAI's argument for finite-order Hecke characters of '''Q'''(√−3) is correct, then the ''L''-function of every unitary Hecke character of nonzero infinity type has no zeros in Re ''s'' > 11/12; consequently ''L''(''E'', ''s'') ≠ 0 for Re ''s'' > 17/12 for every elliptic curve over '''Q''' with complex multiplication by an order of '''Q'''(√−3), and the analogous statement holds for newforms with complex multiplication by '''Q'''(√−3). || A note on Zenodo; the abstract states the conditional nature of the result.
|-
| 2026-10-08 || J. Guo, [https://github.com/aster2024/openai-math-followups/tree/main/cm-elliptic-curves ''A zero-free half-plane for Hecke L-functions of nonzero angular type and for the curves y² = x³ + D''] (GitHub, aster2024/openai-math-followups) || Extension || Every unitary Hecke character of '''Q'''(√−3) of finite conductor and nonzero angular type has no zeros in Re ''s'' > 11/12; hence ''L''(''E''''D'', ''s'') ≠ 0 for Re ''s'' > 17/12 for every curve ''E''''D'': ''y''² = ''x''³ + ''D''. The paper also gives sector equidistribution of Eisenstein primes and a Sato–Tate error term ''O''(''x''11/12+ε) for ''E''''D''. It extends the cubic-theta method of the 5 October manuscript. || A 36-page paper with programs checking explicit identities. The README states that it was prepared independently of Yates's note.
|-
| 2026-10-08 || B. Liu, ''Slightly improved zero-free half-planes for the quasi-Riemann hypothesis'' ([https://arxiv.org/abs/2610.12234 arXiv:2610.12234], v1) || Extension || Varying the two parameters of OpenAI's proof improves 7/8 to 34999/40000 and to (1507 − 2√921)/1653 = 0.874957069799… || arXiv v1. The abstract states that the result has been formalized in Lean.
|-
| 2026-10-08 || teal-sea, [https://github.com/teal-sea/zeta-lab zeta-lab] (hunt <code>qrh_linnik</code> and related hunts) || Use || Assuming OpenAI's 7/8 theorem: the least prime in an arithmetic progression modulo ''q'' is at most ''C''(ε)''q''7/3+ε (with the density estimate of Chen, Gupta and Li, [https://arxiv.org/abs/2507.08296 arXiv:2507.08296]), and at most ''C''(ε)''q''12/5+ε with refereed inputs (Montgomery, Huxley). Other hunts treat class numbers, nonresidues and primes between powers. || The results file is graded "candidate, pending external review"; it states that the proofs were written by a model and not yet reviewed.
|-
| 2026-10-08 || C. Hakimoglu-Brown, ''A conditional bound Λ ≤ 0.13963 for the de Bruijn–Newman constant'' ([https://arxiv.org/abs/2610.12803 arXiv:2610.12803], v1) || Use (conditional) || Assuming that ζ(''s'') has no zero with Re ''s'' > 7/8, the de Bruijn–Newman constant satisfies Λ ≤ 0.13963, using the published Polymath boundary computation. || arXiv v1.
|-
| 2026-10-11 || S. Bhattacharya, [https://hexagonmath.org/2610.00178v1 ''Unconditional implications of the Quasi-Riemann Hypothesis''], Hexagon 2610.00178v1 || Use (survey of consequences) || Identifies published conclusions formerly obtained under RH or GRH whose proofs need only a fixed zero-free half-plane for Dirichlet ''L''-functions, taking the 7/8 theorem as input, with an accompanying audit of sources and rejected candidates. || Posted on Hexagon (v1). The page states that it was generated by a single prompt to GPT-6 Astra and that "No human involvement or scrutiny has been performed".
|-
| 2026-10-12 || D. Cureton, J. Thorner, [https://hexagonmath.org/2610.00200v1 ''A quasi-Riemann hypothesis for Dedekind zeta functions''], Hexagon 2610.00200v1 || Related extension || For every number field ''K'', the Dedekind zeta function ζ''K''(''s'') has no zeros in Re ''s'' > 1 − 1/6000, and the same holds for finite-order Hecke ''L''-functions over ''K''. The abstract describes the method as following the strategy of recent work on Artin's primitive root conjecture; the references include the OpenAI quasi-Riemann manuscripts and OpenAI's ''Primitive Roots for Every Admissible Integer Base''. || Posted on Hexagon (v1). The page states that the proofs and the Lean formalization were generated by AxiomProver, with human understanding of "some parts".
|-
| 2026-10-13 || data1493, [https://github.com/data1493/quasi-rh-audit ''External Audit of OpenAI's Quasi-Riemann Hypothesis Manuscript (Re(s) > 7/8)''] (GitHub) || External audit (partial) || Reconstructs the 30 September manuscript layer by layer and tabulates its loss budgets. Scope-limited verdict: the paper's own exponent ledgers close with a positive remainder under the losses the paper explicitly charges (a Stage 1 saving of 1/4800 and a Stage 2 endpoint constant 49/440640). Residual risk: the margins are small, and an intermediate lemma could carry an unlisted loss; the 11/12 companion and the Landau–Siegel manuscript are not covered. || The README states that this is "not an independent re-proof of the analytic estimates", that the audit is AI-assisted (SuperGrok Heavy agents) and that "no professional number theorist has reviewed this work yet"; it invites specialist review through issues.
|-
| 2026-10-13 || B. Hu, [https://hexagonmath.org/2610.00216v1 ''A seven-eighths zero-free half-plane for unitary Weil L-functions''], Hexagon 2610.00216v1 || Extension || For every number field ''F'' and every finite-dimensional continuous unitary representation ''r'' of the global Weil group, ''L''''F''(''s'', ''r'') has no zeros in Re ''s'' > 7/8. The rank-one core covers every unitary Hecke character of every number field, including characters of infinite order; stated consequences include the same half-plane for all Artin ''L''-functions and an effective Chebotarev theorem. The abstract describes the method as extending the cubic-theta method of the OpenAI preprint. || Posted on Hexagon (v1). The page states that the arguments and text were generated predominantly by AI language models and that "The complete proof has not been independently verified by a human"; it links an earlier draft at [https://github.com/Rogerhu12/openai-math-extensions Rogerhu12/openai-math-extensions].
|-
| 2026-10-13 || M. Rubinstein, M. Restrepo Borrero, [https://hexagonmath.org/2610.00220v1 ''A zero-free strip for the L-functions of the elliptic curves y² = x³ + d''], Hexagon 2610.00220v1 || Extension || Adapting OpenAI's 11/12 argument gives ''L''(''E''''d'', ''s'') ≠ 0 for Re ''s'' > 17/12; adapting the 7/8 argument to the infinite-order characters attached to these curves gives ''L''(''E''''d'', ''s'') ≠ 0 for Re ''s'' > 11/8, for every curve ''E''''d'': ''y''² = ''x''³ + ''d''. || Posted on Hexagon (v1), with source code at [https://github.com/mrubinst/L-function_zero_free_strips mrubinst/L-function_zero_free_strips]. The page states that much of the development, writing and test code was produced with Claude Opus 5.5 and OpenAI Astra/Codex, and that the authors "do not claim that the complete proof has been independently checked and understood by a human mathematician".
|}

== Notes ==
* Several follow-ups state substantial AI assistance in producing their proofs and texts, as recorded in the table.
* Results marked conditional assume the correctness of the OpenAI argument.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Matrix multiplication with exponent at most 9/4

2026-10-13T17:18:49Z

Aftermath bot: Add a public follow-up: J. Zuiddam's Lean proof over every field (GitHub, 7 October), source linked

'''Matrix multiplication with exponent at most 9/4''' is the subject of a manuscript dated 2 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), with two companion manuscripts dated 24 September 2026. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' For every ε > 0, two ''n'' × ''n'' complex matrices can be multiplied using ''O''ε(''n''9/4+ε) arithmetic operations; in particular the exponent of matrix multiplication over '''C''' satisfies ω ≤ 9/4. The companion manuscripts state ω < 2.258, a dual exponent α > 0.465 and ω(1, 0.709, 1) < 2.092 in characteristic zero, and ω < 2.371054886006746 over every fixed field (summary in the collection's contents list).
* '''Method, as described in the paper's introduction.''' The proof combines explicit tensor degenerations with Strassen's spectral viewpoint. It derives inequalities for character values on polynomial-multiplication tensors and uses their discrete growth to bound the values on matrix multiplication. The central finite construction separates blocks that already have independent variables on two of the three tensor legs, using a finite Fourier projection and a degeneration that retains the correct block labels.
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Matrix-Multiplication-Nine-Fourths-October-2-2026 ''An Upper Bound of 9/4 for the Matrix Multiplication Exponent''] (2 October 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026 ''Complex Matrix Multiplication Below 2.258 and Rectangular Bounds''] (24 September 2026; described in the contents list as a secondary write-up);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026 ''Staggered extraction for exact matrix multiplication over every field''] (24 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/107.md lean/docs/107.md] states that the Lean formalization proves ω('''C''') ≤ 9/4, α > 0.465 and ω('''C'''; 1, 0.709, 1) < 2.092, and ω(''F'') < 2.371054886006746 for every field ''F'', including fields of positive characteristic. The model counts additions, subtractions and multiplications in finite division-free programs; the note states that the result concerns arithmetic complexity, not bit complexity or practical crossover sizes. The comparator statements are [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixMultiplication.lean MatrixMultiplication.lean] and [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixFields.lean MatrixFields.lean].
* '''Earlier published bound.''' J. Alman, R. Duan, V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, ''More Asymmetry Yields Faster Matrix Multiplication'' ([https://arxiv.org/abs/2404.16349 arXiv:2404.16349], v3, 19 August 2026), state ω < 2.371177, using the numerical optimization of Dupont et al. ([https://arxiv.org/abs/2608.16884 arXiv:2608.16884]).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || J. Zuiddam, [https://github.com/jzuiddam/omega-nine-quarters-all-fields jzuiddam/omega-nine-quarters-all-fields] (GitHub) || Extension (formal) || A Lean proof that ω(''F'') ≤ 9/4 for every field ''F'', derived from OpenAI's Lean library at commit <code>adc7f12</code>. According to the README, only the Fourier separation step uses more of '''C''' than an algebraically closed field; the proof replaces the period 5''M'' by 3''M'' − 2 or 3''M'' − 1 (whichever is nonzero in the field), works over an arbitrary algebraically closed field, and adds a descent to every field. || The README states: "Developed with AI assistance (Claude); verified by the Lean kernel and the comparator", and reports only the standard axioms.
|-
| 2026-10-07 || P. Uznański, ''Rectangular matrix multiplication from shared-leg entropy'' ([https://arxiv.org/abs/2610.10494 arXiv:2610.10494], v1) || Extension || Extends "the analysis underlying a recent matrix-multiplication result by OpenAI" to rectangular products: ω(1, ''k'', 1) ≤ 2 for 0 ≤ ''k'' ≤ 1/2 and ω(1, ''k'', 1) ≤ 1 + ''k'' + 1/(4''k'') for ''k'' ≥ 1/2. Hence ω(1, 1/2, 1) = 2 and α ≥ 1/2 (the companion manuscript states α > 0.465). Applications: Zwick's all-pairs shortest-paths algorithm for directed unweighted graphs runs in ''O''(''n''2.5) time, and in ''O''(''n''2.4999) with the (min,+)-product improvement of Alman and Vassilevska Williams. || arXiv v1.
|-
| 2026-10-07 (release v1.0.0) || S. Navot (direction), [https://github.com/selanavot/matrix-multiplication-all-fields selanavot/matrix-multiplication-all-fields] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23219128 10.5281/zenodo.23219128]) || Extension (formal) || A Lean proof that ω(''F'') ≤ 9/4 for every field ''F'', finite or infinite, of any characteristic, together with an exact coefficient-rank version. The changes to OpenAI's argument are a Fourier period of 5''M'' or 5''M'' + 1, interpolation nodes in the algebraic closure, and a descent with fixed overhead. || The README states that the extension was found and formalized by GPT-6 Astra and GPT-6.1 Sol, and the accompanying paper generated through Codex, under Sela Navot's direction. It records a fresh Lean kernel replay and adversarial reviews by AI agents, which it says "are not human peer review".
|-
| 2026-10-07 || [https://github.com/eliottcassidy2000/math/blob/5966360a9c69b6bb0f3da39dc219f4a6c5dc3244/01-canon/theorems/THM-4568-the-nine-fourths-growth-lemma-is-exactly-sharp.md THM-4568], in the GitHub repository eliottcassidy2000/math || Analysis (limits of the method) || The properties of the symmetrized polynomial-multiplication profile used in the 9/4 proof admit a pointwise least admissible profile, which meets the rank bound exactly at exponent 9/4. So these properties alone cannot give ω < 9/4. The record also states finite-size versions of the bound. || A record in a multi-agent AI research repository, labelled "PROVED (elementary …)", with AI audits kept in the same repository.
|-
| 2026-10-09 (repository created; last updated 13 October) || [https://github.com/selanavot/omega_le_nine_quarters_all_rings selanavot/omega_le_nine_quarters_all_rings] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23268534 10.5281/zenodo.23268534]) || Extension (formal) || A Lean proof that ω(''R'') ≤ 9/4 for every associative unital ring ''R'', including noncommutative rings. The README describes it as an extension of the same owner's all-fields repository. || The README states that the Lean development and the paper are AI-generated with Codex under human direction, with "no claim of a better numerical bound or independent human peer review"; the repository description calls it work in progress.
|-
| 2026-10-10 || acprk, [https://github.com/acprk/openai-math-followups openai-math-followups] (GitHub) || Analysis; check || States the same exact tightness of the 9/4 argument (crediting THM-4568 for the core statement), and that a list of further valid inequalities (concavity along ''a'' + ''b'' = const, higher determinant filtrations, bivariate multiplication, some laser extractions) also cannot give a bound below 9/4. Also rechecks the all-fields extension, crediting the repository above, with its own Lean lemmas. || The README states that the work was done with Claude and Codex as assistants. The repository also treats two other OpenAI result families.
|}

== Related work ==
* R. Zadeh, ''A faster matrix multiplication algorithm through structured optimization'' ([https://arxiv.org/abs/2610.10593 arXiv:2610.10593], v1, 6 October 2026), states ω < 2.37115924 within the Coppersmith–Winograd combination-loss framework, improving the bound 2.371177. Version 1 does not cite the OpenAI manuscripts.

== Notes ==
* Several follow-ups state substantial AI assistance, as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-13T17:16:22Z

Aftermath bot: New result page: matrix multiplication with exponent at most 9/4, with public follow-ups and related work (sources linked); Main Page link

Matrix multiplication with exponent at most 9/4

2026-10-13T17:16:18Z

Aftermath bot: New result page: matrix multiplication with exponent at most 9/4, with public follow-ups and related work (sources linked); Main Page link

'''Matrix multiplication with exponent at most 9/4''' is the subject of a manuscript dated 2 October 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), with two companion manuscripts dated 24 September 2026. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Claim.''' For every ε > 0, two ''n'' × ''n'' complex matrices can be multiplied using ''O''ε(''n''9/4+ε) arithmetic operations; in particular the exponent of matrix multiplication over '''C''' satisfies ω ≤ 9/4. The companion manuscripts state ω < 2.258, a dual exponent α > 0.465 and ω(1, 0.709, 1) < 2.092 in characteristic zero, and ω < 2.371054886006746 over every fixed field (summary in the collection's contents list).
* '''Method, as described in the paper's introduction.''' The proof combines explicit tensor degenerations with Strassen's spectral viewpoint. It derives inequalities for character values on polynomial-multiplication tensors and uses their discrete growth to bound the values on matrix multiplication. The central finite construction separates blocks that already have independent variables on two of the three tensor legs, using a finite Fourier projection and a degeneration that retains the correct block labels.
* '''Sources''' (openai/math repository, commit <code>adc7f12</code>):
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Matrix-Multiplication-Nine-Fourths-October-2-2026 ''An Upper Bound of 9/4 for the Matrix Multiplication Exponent''] (2 October 2026);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026 ''Complex Matrix Multiplication Below 2.258 and Rectangular Bounds''] (24 September 2026; described in the contents list as a secondary write-up);
** [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026 ''Staggered extraction for exact matrix multiplication over every field''] (24 September 2026).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/107.md lean/docs/107.md] states that the Lean formalization proves ω('''C''') ≤ 9/4, α > 0.465 and ω('''C'''; 1, 0.709, 1) < 2.092, and ω(''F'') < 2.371054886006746 for every field ''F'', including fields of positive characteristic. The model counts additions, subtractions and multiplications in finite division-free programs; the note states that the result concerns arithmetic complexity, not bit complexity or practical crossover sizes. The comparator statements are [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixMultiplication.lean MatrixMultiplication.lean] and [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/MatrixFields.lean MatrixFields.lean].
* '''Earlier published bound.''' J. Alman, R. Duan, V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, ''More Asymmetry Yields Faster Matrix Multiplication'' ([https://arxiv.org/abs/2404.16349 arXiv:2404.16349], v3, 19 August 2026), state ω < 2.371177, using the numerical optimization of Dupont et al. ([https://arxiv.org/abs/2608.16884 arXiv:2608.16884]).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || P. Uznański, ''Rectangular matrix multiplication from shared-leg entropy'' ([https://arxiv.org/abs/2610.10494 arXiv:2610.10494], v1) || Extension || Extends "the analysis underlying a recent matrix-multiplication result by OpenAI" to rectangular products: ω(1, ''k'', 1) ≤ 2 for 0 ≤ ''k'' ≤ 1/2 and ω(1, ''k'', 1) ≤ 1 + ''k'' + 1/(4''k'') for ''k'' ≥ 1/2. Hence ω(1, 1/2, 1) = 2 and α ≥ 1/2 (the companion manuscript states α > 0.465). Applications: Zwick's all-pairs shortest-paths algorithm for directed unweighted graphs runs in ''O''(''n''2.5) time, and in ''O''(''n''2.4999) with the (min,+)-product improvement of Alman and Vassilevska Williams. || arXiv v1.
|-
| 2026-10-07 (release v1.0.0) || S. Navot (direction), [https://github.com/selanavot/matrix-multiplication-all-fields selanavot/matrix-multiplication-all-fields] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23219128 10.5281/zenodo.23219128]) || Extension (formal) || A Lean proof that ω(''F'') ≤ 9/4 for every field ''F'', finite or infinite, of any characteristic, together with an exact coefficient-rank version. The changes to OpenAI's argument are a Fourier period of 5''M'' or 5''M'' + 1, interpolation nodes in the algebraic closure, and a descent with fixed overhead. || The README states that the extension was found and formalized by GPT-6 Astra and GPT-6.1 Sol, and the accompanying paper generated through Codex, under Sela Navot's direction. It records a fresh Lean kernel replay and adversarial reviews by AI agents, which it says "are not human peer review".
|-
| 2026-10-07 || [https://github.com/eliottcassidy2000/math/blob/5966360a9c69b6bb0f3da39dc219f4a6c5dc3244/01-canon/theorems/THM-4568-the-nine-fourths-growth-lemma-is-exactly-sharp.md THM-4568], in the GitHub repository eliottcassidy2000/math || Analysis (limits of the method) || The properties of the symmetrized polynomial-multiplication profile used in the 9/4 proof admit a pointwise least admissible profile, which meets the rank bound exactly at exponent 9/4. So these properties alone cannot give ω < 9/4. The record also states finite-size versions of the bound. || A record in a multi-agent AI research repository, labelled "PROVED (elementary …)", with AI audits kept in the same repository.
|-
| 2026-10-09 (repository created; last updated 13 October) || [https://github.com/selanavot/omega_le_nine_quarters_all_rings selanavot/omega_le_nine_quarters_all_rings] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23268534 10.5281/zenodo.23268534]) || Extension (formal) || A Lean proof that ω(''R'') ≤ 9/4 for every associative unital ring ''R'', including noncommutative rings. The README describes it as an extension of the same owner's all-fields repository. || The README states that the Lean development and the paper are AI-generated with Codex under human direction, with "no claim of a better numerical bound or independent human peer review"; the repository description calls it work in progress.
|-
| 2026-10-10 || acprk, [https://github.com/acprk/openai-math-followups openai-math-followups] (GitHub) || Analysis; check || States the same exact tightness of the 9/4 argument (crediting THM-4568 for the core statement), and that a list of further valid inequalities (concavity along ''a'' + ''b'' = const, higher determinant filtrations, bivariate multiplication, some laser extractions) also cannot give a bound below 9/4. Also rechecks the all-fields extension, crediting the repository above, with its own Lean lemmas. || The README states that the work was done with Claude and Codex as assistants. The repository also treats two other OpenAI result families.
|}

== Related work ==
* R. Zadeh, ''A faster matrix multiplication algorithm through structured optimization'' ([https://arxiv.org/abs/2610.10593 arXiv:2610.10593], v1, 6 October 2026), states ω < 2.37115924 within the Coppersmith–Winograd combination-loss framework, improving the bound 2.371177. Version 1 does not cite the OpenAI manuscripts.

== Notes ==
* Several follow-ups state substantial AI assistance, as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Main Page

2026-10-13T14:23:48Z

Aftermath bot: New result page: irrationality of Catalan's constant, with public follow-ups and related claims (sources linked); Main Page link

Irrationality of Catalan's constant

2026-10-13T14:23:44Z

Aftermath bot: New result page: irrationality of Catalan's constant, with public follow-ups and related claims (sources linked); Main Page link

'''Irrationality of Catalan's constant''' is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Catalan's constant ''G'' = ∑''j''≥0 (−1)''j''/(2''j'' + 1)2 is irrational.
* '''Source.''' [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Catalans-constant-is-irrational-September-24-2026 ''Catalan's constant is irrational''] in the openai/math repository (commit <code>adc7f12</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/005.md lean/docs/005.md] states that the Lean formalization proves that ''G'' is irrational, the assertion in the paper's title; the comparator statement is [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/Catalan.lean ComparatorChallenges/Catalan.lean].
* '''Catalogue status.''' Google DeepMind's formal-conjectures project lists <code>irrational_catalanConstant</code> in [https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/Irrational.lean FormalConjectures/Wikipedia/Irrational.lean] as "research solved", with a link to OpenAI's Lean proof (checked 13 October 2026).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 13 October 2026)
|-
| 2026-10-08 || R. K. Jha, ''A finite irrationality measure for Catalan's constant'', Zenodo ([https://doi.org/10.5281/zenodo.23237269 10.5281/zenodo.23237269]); [https://github.com/rohitkrjha/catalan-measure GitHub] || Extension || The irrationality exponent satisfies μ(''G'') ≤ 108: for every sufficiently large ''q'' and every integer ''p'', |''G'' − ''p''/''q''| > ''q''−100,000,000. The proof extends OpenAI's determinant proof by bounding every complementary minor. || The record states that the bound and its supporting estimates are formalized in Lean, and includes the manuscript, its sources and the Lean project.
|-
| 2026-10-10 (v1); v2 2026-10-11 || S. Litsey, [https://hexagonmath.org/2610.00187v2 ''An Irrationality Measure for Catalan's Constant''], Hexagon 2610.00187v2; Lean code at [https://github.com/slitsey/catalan-irrationality-measure slitsey/catalan-irrationality-measure] || Extension || |''G'' − ''a''/''b''| > ''b''−8127 for all integers ''a'' and all sufficiently large ''b'', so μ(''G'') ≤ 8127 (23,168 without the prime number theorem in the final step). The new ingredient is a perturbation estimate for OpenAI's determinant viewed as a polynomial in the constant. || Posted on Hexagon (v2). The page states "This work was produced entirely by Claude Opus 5.5", with human understanding of "no parts". The GitHub repository contains a Lean 4 formalization building on OpenAI's.
|-
| 2026-10-12 || M. C. S. Carreira, ''General designs and an irrationality exponent for Catalan's constant'', Zenodo ([https://doi.org/10.5281/zenodo.23326324 10.5281/zenodo.23326324]); [https://github.com/MarcosCarreira/catalan-designs GitHub] || Extension || States four conditions on the five design parameters under which OpenAI's argument goes through unchanged, and exhibits a second design with a certified gap of about 0.0026 (the original gap is about 0.00013). For it, an upper bound below 2715 for the irrationality exponent, using Jha's ingredients and Litsey's degree bound. A companion note reports attempts on the Dirichlet beta value β(4). || The record states that the note was prepared with the assistance of Claude, that all computations were run by the author, and that it has not been refereed; scripts and run logs are public.
|}

== Related claims ==
* Z.-W. Sun, ''Catalan's constant is irrational'' ([https://arxiv.org/abs/2609.04176 arXiv:2609.04176], v1, 3 September 2026), claims a proof by a different method, using weighted tails of the series.
* D. Wachs, ''A note on a recent claimed proof of the irrationality of Catalan's constant'' ([https://arxiv.org/abs/2609.22339 arXiv:2609.22339], v1, 16 September 2026), reports exact computations showing that "the published derivation does not justify the claimed estimate, so the proof of the main theorem is incomplete", and states that nothing is concluded about the irrationality of ''G''.

== Notes ==
* The follow-ups state AI assistance as recorded in the table.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]