# Nonnegative-curvature Einstein classification and an <i>L</i><sup>2</sup> topological gap

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

- [Positively curved Einstein four-manifolds](../../preprints/Positively-curved-Einstein-four-manifolds-September-23-2026/paper.pdf)

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

| Result | Comparator statement |
| --- | --- |
| Classification of positively curved Einstein four-manifolds | [EinsteinFour.lean](../ComparatorChallenges/EinsteinFour.lean) |