Browse › Differential geometry › 348 Nonnegative-curvature Einstein classification and an L2 topological gap
Positively curved Einstein four-manifolds
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove the classification conjecture for connected smooth closed Einstein four-manifolds with strictly positive sectional curvature. Up to positive scaling and isometry, every such manifold is the round four-sphere, the complex projective plane with its Fubini–Study metric, or real projective four-space with its round metric. No orientability assumption is needed.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope note 348: Nonnegative-curvature Einstein classification and an L² topological gap (lean/docs/348.md, 2026). The scope note names this manuscript and says the Lean development covers its classification theorem (round S⁴, Fubini–Study CP², round RP⁴, no orientability assumption), linking to a comparator statement.
- OpenAI math release, EinsteinFour.lean (comparator challenge statement) (github.com/openai/math, commit adc7f12, 2026). Target statements
orientedClassification,classificationOnandclassificationfor this paper's main theorem, stated there withsorryas the challenge to be matched. - OpenAI math release, OAI/Geometry/EinsteinFour/Classification.lean (github.com/openai/math, commit adc7f12, 2026). Solution module stating
classificationfor this paper's Theorem 1.1; its proof callsclassificationOnfrom imported modules.
Possibly relevant literature (found by the agent, not checked)
- Z. Zhang, Four-dimensional Einstein manifolds with sectional curvature bounded from above (arXiv:1606.01157, 2016). Proves that a nonnegatively curved Einstein four-manifold satisfying a pinching condition is S⁴, RP⁴ or CP²; this is another quantitative upper-bound result in the line (Yang, Costa, Cao–Tran) surveyed in the introduction, and it is not cited.
- T. Liu, Toric Einstein 4-manifolds with nonnegative sectional curvature (arXiv:2311.04840; Ann. Global Anal. Geom. 67 (2025), 14). Shows that T²-invariant Einstein metrics with nonnegative sectional curvature are locally symmetric; this symmetry-based partial result is cited in the companion papers but not here, next to the Killing-field corollary of Cheng.
Digests and expositions
- Latent Seminar, Einstein four-manifolds: curvature rigidity and an L² topological gap (7 October 2026). Explains the three manuscripts’ dependencies, coupled Weyl estimates and Ricci-flow gap argument, and distinguishes its reported arithmetic checks from verification of the complete proofs. [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 348
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Positively-curved-Einstein-four-manifolds-September-23-2026,
author = {{OpenAI}},
title = {{Positively curved Einstein four-manifolds}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Positively-curved-Einstein-four-manifolds-September-23-2026/paper.pdf}{OAI:Positively-curved-Einstein-four-manifolds-September-23-2026}},
year = {2026}
}From OpenAI's README for this paper:
Verification
The exact-arithmetic checker requires Python 3.10 or later and only the standard library. Run from this paper directory:
python3 -B verification/verify.py --check
Success means exit status zero and all_passed: true, with 53 identities, 15 reported univariate certificate rows plus 6 supplementary rows, 12 triangle certificate rows, and 24 additional exact-value assertions. The command recomputes the complete deterministic result and compares it with verification/results.json.
These are finite arithmetic checks, not a proof-assistant formalization of the whole argument. The precise scope and its distinction from the mathematical reductions proved in the paper are recorded in verification/COVERAGE.md. Additional package-level reproduction instructions are in verification/README.md.
Lean formalization
OpenAI provides Lean files for this family: lean/docs/348.md. The Lean statements have not been checked by people against the paper's claims.
Family 348: Nonnegative-curvature Einstein classification and an L2 topological gap
Classifies closed connected Einstein four-manifolds with positive Einstein constant and nonnegative sectional curvature: up to scaling, their universal Riemannian covers are the round S4, Fubini–Study $\mathbb{CP}^2$, or a product of equal round two-spheres. A closed simply connected nonnegatively curved four-manifold is diffeomorphic to one of these whenever the scale-invariant L2 norm of its trace-free Ricci curvature lies below a universal positive constant.
Other papers in this family:
- Zero-Plane Rigidity for Einstein Four-Manifolds · October 4, 2026
- An L² Einstein Gap for Nonnegatively Curved Four-Manifolds · October 5, 2026