∑math20

Differential geometry · Result 348

Nonnegative-curvature Einstein classification and an L2 topological gap

3 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 3

First page of Zero-Plane Rigidity for Einstein Four-Manifolds

Zero-Plane Rigidity for Einstein Four-Manifolds

OpenAI · October 4, 2026

We prove that a closed Einstein four-manifold with positive Einstein constant, nonnegative sectional curvature, and a zero-curvature plane has universal Riemannian cover isometric to a product of two round two-spheres. Under the normalization \(\mathop{\mathrm{Ric}}\nolimits =3g\), both spheres have radius \(1/\sqrt3\). The proof extends coupled estimates for the two Weyl curvature blocks to the boundary of the sectional-curvature cone and determines their equality case.

Read PDF Download Source

Cite
@misc{OAI:Zero-Plane-Rigidity-for-Einstein-Four-Manifolds-October-4-2026,
  author = {{OpenAI}},
  title = {{Zero-Plane Rigidity for Einstein Four-Manifolds}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Zero-Plane-Rigidity-for-Einstein-Four-Manifolds-October-4-2026/einstein-boundary.pdf}{OAI:Zero-Plane-Rigidity-for-Einstein-Four-Manifolds-October-4-2026}},
  year = {2026}
}
First page of An L² Einstein Gap for Nonnegatively Curved Four-Manifolds

An L² Einstein Gap for Nonnegatively Curved Four-Manifolds

OpenAI · October 5, 2026

We prove a universal, scale-invariant L2 gap for the trace-free Ricci tensor on simply connected closed four-manifolds with nonnegative sectional curvature. If the trace-free Ricci energy is sufficiently small, the manifold is diffeomorphic to S4, \(\mathbb{CP}^2\), or \(S^2\times S^2\). The proof uses the classification of positive-Einstein, nonnegatively curved four-manifolds supplied by the companion zero-plane rigidity theorem, stated explicitly as the classification premise of our result. No auxiliary curvature, volume, diameter, injectivity-radius, or Sobolev bound is required. The conclusion concerns the smooth manifold, not an isometry of the original metric.

Read PDF Download Source

Cite
@misc{OAI:An-L2-Einstein-Gap-for-Nonnegatively-Curved-Four-Manifolds-October-5-2026,
  author = {{OpenAI}},
  title = {{An $L^2$ Einstein Gap for Nonnegatively Curved Four-Manifolds}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-L2-Einstein-Gap-for-Nonnegatively-Curved-Four-Manifolds-October-5-2026/einstein-gap.pdf}{OAI:An-L2-Einstein-Gap-for-Nonnegatively-Curved-Four-Manifolds-October-5-2026}},
  year = {2026}
}
First page of Positively curved Einstein four-manifolds

Positively curved Einstein four-manifolds

OpenAI · September 23, 2026

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.

Read PDF Download Source

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}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization classifies 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 round real projective four-space. No orientability hypothesis is required. In the oriented case, only the sphere and complex projective plane occur.

Comparator links

ResultComparator statement
Classification of positively curved Einstein four-manifoldsEinsteinFour.lean

Scope note on GitHub →