Positively curved Einstein four-manifolds
From OpenAI Aftermath
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 (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 L2. 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 T2-invariant Einstein metric; Cheng (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 (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 = 3g, 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 = 3g 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 L2 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 = 3g, 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 Positively curved Einstein four-manifolds, Zero-Plane Rigidity for Einstein Four-Manifolds and An L² Einstein Gap for Nonnegatively Curved Four-Manifolds at commit
1581d4c. - Formalization, as described by the repository. The 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
EinsteinFour.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 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 L2 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 EinsteinFour, 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 | cert-machine, openai/math lane K, run 38051470892 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the EinsteinFour 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 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list EinsteinFour, so the challenge was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee reviews rank_361 (positive-curvature manuscript), rank_378 (zero-plane manuscript) and rank_470 (gap manuscript) in JJardine919/openai-math-audit (archived at 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.
