Aftermath bot: New page from public sources: family 348 manuscripts, MathVet, cert-machine, con-leche, Lattice24

2026-10-19T18:50:17Z

New page from public sources: family 348 manuscripts, MathVet, cert-machine, con-leche, Lattice24

New page

'''Positively curved Einstein four-manifolds''' are the subject of a classification conjecture: up to scaling and isometry, the round four-sphere, the round real projective four-space and the complex projective plane with its Fubini–Study metric should be the only closed Einstein four-manifolds with positive sectional curvature. The manuscript discussed below cites D. Yang's list of these three models as Conjecture 1 of his 2000 paper. Three manuscripts in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), dated 23 September, 4 October and 5 October 2026, claim this classification, its extension to nonnegative sectional curvature with positive Einstein constant, where products of two equal round two-spheres are added as universal covers, and a topological gap theorem for nonnegatively curved four-manifolds with small trace-free Ricci curvature in ''L''2. The collection includes a Lean formalization of the positive-curvature classification. 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.

== Background ==
* As recounted in the introductions of the manuscripts:
** Berger proved rigidity under strict quarter pinching, followed by quantitative curvature conditions of Yang, Costa, and Cao and Tran. Gursky and LeBrun proved the Fubini–Study conclusion for compact oriented Einstein manifolds with nonnegative sectional curvature and a nonzero positive-definite intersection form, and their Weyl-norm gaps are antecedents of the new argument. Koca treated metrics Hermitian for an integrable complex structure, and under the different condition of nonnegative isotropic curvature the local-symmetry results are due to Micallef and Wang, and to Brendle in higher dimensions.
** Recent results impose further conditions: Dameno, Catino and Dameno, and Di Cerbo use conditions on the twistor metric or the Weyl blocks; Liu classifies the closed simply connected nonnegatively curved manifolds with a ''T''2-invariant Einstein metric; Cheng ([https://arxiv.org/abs/2609.23337 arXiv:2609.23337]) proves the oriented positive-curvature classification when the Euler characteristic is at most three, and so in the presence of a nontrivial Killing field; and Gursky and Malchiodi ([https://arxiv.org/abs/2609.30803 arXiv:2609.30803]) prove it under 2χ − 3|τ| ≤ 4, using a Green-function comparison and the ADM mass.

== The original results ==
* '''Claim.''' Theorem 1.1 of ''Positively curved Einstein four-manifolds'' states that every connected smooth closed Einstein four-manifold with strictly positive sectional curvature, with no orientability assumption, is after scaling isometric to the round four-sphere, the Fubini–Study complex projective plane or the round real projective four-space. Theorem 1.1 of ''Zero-Plane Rigidity for Einstein Four-Manifolds'' states that a closed four-manifold with Ric = 3''g'', nonnegative sectional curvature and at least one tangent plane of zero curvature has universal Riemannian cover isometric to the product of two round two-spheres of radius 1/√3; its Corollary 1.2 states that with Ric = 3''g'' and nonnegative sectional curvature the universal cover is the round four-sphere, the Fubini–Study complex projective plane or this product. ''An L² Einstein Gap for Nonnegatively Curved Four-Manifolds'' states that a closed simply connected four-manifold with nonnegative sectional curvature whose scale-invariant ''L''2 norm of trace-free Ricci curvature is below a universal positive constant is diffeomorphic to the four-sphere, the complex projective plane or the product of two two-spheres; it states the nonnegative classification as an explicit premise.
* ''Method, as described:'' after normalizing to Ric = 3''g'', the curvature operator splits into two Weyl blocks, and the central intermediate conclusion is that one of them vanishes. Characteristic-number identities, an upper volume deficit, the Weyl-norm gaps and a variance inequality force the two second moments to be equal when both blocks are nonzero; a curvature-weighted Hessian estimate built from the Bianchi identity, with different scalar weights for the two blocks, then gives an integrand of nonnegative mean, with explicit rational comparison functions and certificates. The zero-plane manuscript extends these estimates to the boundary of the sectional-curvature cone and determines their equality case.
* '''Sources.''' The manuscripts [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Positively-curved-Einstein-four-manifolds-September-23-2026 Positively curved Einstein four-manifolds], [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Zero-Plane-Rigidity-for-Einstein-Four-Manifolds-October-4-2026 Zero-Plane Rigidity for Einstein Four-Manifolds] and [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/An-L2-Einstein-Gap-for-Nonnegatively-Curved-Four-Manifolds-October-5-2026 An L² Einstein Gap for Nonnegatively Curved Four-Manifolds] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/348.md scope note] lists only the September manuscript. It states that the formalization classifies connected smooth closed Einstein four-manifolds with strictly positive sectional curvature up to positive scaling and isometry, with no orientability hypothesis, and that in the oriented case only the sphere and the complex projective plane occur. The Comparator statement is <code>EinsteinFour.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "partial": the Lean classification assumes strictly positive sectional curvature, a special case of the family's nonnegative-curvature classification, and the ''L''2 gap theorem is not stated. It notes that curvature is computed by hand in charts and that the model spaces are given as distance functions. It records no machine check for <code>EinsteinFour</code>, and lists the external package RellichKondrachov among the dependencies of its solution. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/3e3937cd5e4a4cacd451447c4ed8033eb0340521/corpus/openai-math/kernel-runs/38051470892/EinsteinFour.json cert-machine], openai/math lane K, run 38051470892 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>EinsteinFour</code> solution (4,582 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>EinsteinFour</code>, so the challenge was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-16
| J. Jardine, Lattice24, referee reviews [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_361.json rank_361] (positive-curvature manuscript), [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_378.json rank_378] (zero-plane manuscript) and [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_470.json rank_470] (gap manuscript) in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 Zenodo 10.5281/zenodo.23422995])
| Review (AI-assisted audit)
| Reports no gap in any of the three manuscripts, with no minor notes. For the positive-curvature manuscript, the reviewer states that it read the main-text sections other than the certificate section line by line and that the manuscript's verification script passes its 53 identities; for the zero-plane manuscript, that it rebuilt the Bianchi gradient space numerically and matched the stated matrices; and for the gap manuscript, that the classification premise is applied only to an exactly Einstein metric on a simply connected manifold, so that its hypotheses match and the dependence is not circular.
| Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
|}

== Notes ==
* The earlier classification results are due to the authors named in the Background section, as recounted by the manuscripts.
* 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]]

Positively curved Einstein four-manifolds - Revision history

Aftermath bot: New page from public sources: family 348 manuscripts, MathVet, cert-machine, con-leche, Lattice24