OpenAI claim summary for Math-215
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
A topological Einstein-energy gap: The L2 gap explicitly assumes the Einstein classification and requires sufficiently small traceless-Ricci energy.
Positive-Einstein four-manifold classification: The classification requires an Einstein metric and real dimension four.
Zero-plane Einstein rigidity: The classification requires an Einstein metric and real dimension four.
This page records partial support. Complete resolution of the catalogue question is not established by this record.
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Hopf Conjecture
OpenAI's claim
A topological Einstein-energy gap: Assuming the manuscript's normalized classification of nonnegatively curved Einstein four-manifolds, a sufficiently small scale-invariant $L^2$ trace-free Ricci energy is claimed to force a simply connected closed nonnegatively curved four-manifold to be diffeomorphic to $S^4$, $\mathbb{CP}^2$ or $S^2\times S^2$. No additional geometric bounds are imposed.Positive-Einstein four-manifold classification: The paper claims that closed connected positively curved Einstein four-manifolds are, up to scaling, the round sphere, Fubini--Study projective plane, or round real projective space; the last possibility accommodates nonorientability.
Zero-plane Einstein rigidity: The claim assumes a positive Einstein constant on a closed four-manifold; if sectional curvature is nonnegative and one plane is flat, the universal cover is the product of two round constant-curvature surfaces; the radii are fixed by the Einstein normalization.
Mathematical statement of the claimed result
Mathematical claim 1.
Assume the companion classification: every closed connected smooth four-manifold with $\operatorname{Ric}=3g$ and sectional curvature $\ge0$ has universal cover isometric to round $S^4$, Fubini--Study $\mathbb{CP}^2$ normalized by $\operatorname{Ric}=3g$, or $S^2(1/\sqrt3)\times S^2(1/\sqrt3)$. Under that explicit premise, the claim gives an absolute $\epsilon_0>0$ such that any closed connected simply connected smooth four-manifold with $\sec_g\ge0$ and \[\int_M\left|\operatorname{Ric}_g-\tfrac14\operatorname{Scal}_g g\right|^2\,dV_g<\epsilon_0\] is diffeomorphic, without specified orientation, to $S^4$, $\mathbb{CP}^2$ or $S^2\times S^2$. The conclusion is topological rather than isometric, and the theorem is expressly conditional on the classification premise.Mathematical claim 2.
In real dimension four, assume $M$ is smooth, closed and connected, and its metric is Einstein with $\sec_g>0$, there is $a>0$ such that $(M,ag)$ is claimed to be isometric to standard round $S^4$, Fubini--Study $\mathbb{CP}^2$, or standard round $\mathbb{RP}^4$. Einstein means $\operatorname{Ric}=\lambda g$ for a constant $\lambda$. Orientability is not required; the Einstein hypothesis is essential to this statement and is absent from the general Hopf conjecture.Mathematical claim 3.
For a connected smooth closed four-manifold with $\operatorname{Ric}_g=3g$ and sectional curvature $\ge0$, the existence of one zero-curvature tangent two-plane is claimed to force its universal Riemannian cover to be \[S^2(1/\sqrt3)\times S^2(1/\sqrt3).\] Its corollary classifies every such universal cover as this product, round $S^4$ of curvature $1$, or Fubini--Study $\mathbb{CP}^2$ with $\operatorname{Ric}=3g$. This is an Einstein four-dimensional assertion, not a classification of all nonnegatively curved manifolds.Outline of the argument
A topological Einstein-energy gap: A hypothetical countersequence is normalized and shown to satisfy initial geometry and Sobolev bounds. A uniform smoothing interval controls its high-curvature region and propagates the Einstein defect and negative-sectional-curvature error. The limit is a compact nonnegatively curved positive-Einstein space, whose companion classification identifies the topology and contradicts the sequence.Positive-Einstein four-manifold classification: After normalizing the Einstein constant, coupled inequalities track the two Weyl blocks distinguished by the Hodge star. Weighted variance, Hessian, and moment comparisons reduce the analytic step to exact polynomial signs, forcing one block to vanish. Characteristic identities and a volume argument identify the oriented models, followed by an orientation-cover analysis of the possible quotient.
Zero-plane Einstein rigidity: Bonnet--Myers reduces the analysis to the compact simply connected cover. The two Weyl blocks satisfy a sharp coupled spectral constraint at the boundary of the curvature cone. Extending the weighted comparisons to this boundary and tracking equality forces the product geometry rather than merely a weaker norm bound.
Formal verification
Family 348 describes Lean coverage for the strict-positive-curvature Einstein classification; zero-plane rigidity and the small-energy gap are separate.A topological Einstein-energy gap: No manuscript-specific Comparator is listed in the pinned inventory.
The documented selection does not cover the entire manuscript assertion relevant here.
Positive-Einstein four-manifold classification: The manuscript links EinsteinFour.lean.
The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.
Zero-plane Einstein rigidity: No manuscript-specific Comparator is listed in the pinned inventory.
The documented selection does not cover the entire manuscript assertion relevant here.
This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.
Status caveat
OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.Sources
- OpenAI, An L${}^{2}$ Einstein Gap for Nonnegatively Curved Four-Manifolds, 2026-10-05; citation key
OAI:An-L2-Einstein-Gap-for-Nonnegatively-Curved-Four-Manifolds-October-5-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:gap. - OpenAI, Positively curved Einstein four-manifolds, 2026-09-23; citation key
OAI:Positively-curved-Einstein-four-manifolds-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:classification. - OpenAI, Zero-Plane Rigidity for Einstein Four-Manifolds, 2026-10-04; citation key
OAI:Zero-Plane-Rigidity-for-Einstein-Four-Manifolds-October-4-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main; Statement source: cor:nonnegative-classification. - Family 348: Lean scope.
- Comparator EinsteinFour.json.
- Comparator EinsteinFour.lean.
- OpenAI catalogue entry.