Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Lean statement

Classification of positively curved Einstein four-manifolds

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorems selected for verification: OAI.PositiveEinsteinFour.orientedClassification OAI.PositiveEinsteinFour.classificationOn OAI.PositiveEinsteinFour.classification

Lean statement file: EinsteinFour.leanShow on the mapOpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 348 link it.

See the candidate theoremWho ran the proof-verification programReport a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem orientedClassification (X : ClosedOrientedMetricFour.{u})    (hEinstein : IsEinstein X.metric) (hpositive : HasPositiveSectionalCurvature X.metric) :    ∃ a : ℝ, 0 < a ∧ (ScaledIsometricTo X.metric a roundDistance ∨      ScaledIsometricTo X.metric a fubiniStudyDistance) := by  sorrytheorem classificationOn : ClassificationOn M := by  sorrytheorem classification (M : Type*) [TopologicalSpace M] [ChartedSpace FourSpace M]    [IsManifold I4 ∞ M] [T2Space M] [SecondCountableTopology M]    [CompactSpace M] [ConnectedSpace M] (g : SmoothMetric M)    (hEinstein : IsEinstein g) (hpositive : HasPositiveSectionalCurvature g) :    ∃ a : ℝ, 0 < a ∧      (ScaledIsometricTo g a roundDistance ∨        ScaledIsometricTo g a fubiniStudyDistance ∨        ScaledIsometricTo g a realProjectiveDistance) := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

  • abbreviation OAI.EinsteinFour.FourSpace line 12

    abbrev FourSpace := EuclideanSpace ℝ (Fin 4)

  • abbreviation OAI.EinsteinFour.I4 line 13

    abbrev I4 := 𝓘(ℝ, FourSpace)

  • definition OAI.EinsteinFour.coordinateVector line 15

    def coordinateVector (i : Fin 4) : FourSpace := EuclideanSpace.single i 1

  • abbreviation OAI.EinsteinFour.RoundSphere4 line 17

    abbrev RoundSphere4 := {x : EuclideanSpace ℝ (Fin 5) // ‖x‖ = 1}

  • abbreviation OAI.EinsteinFour.ComplexProjective2 line 19

    abbrev ComplexProjective2 := Projectivization ℂ (EuclideanSpace ℂ (Fin 3))

  • abbreviation OAI.EinsteinFour.RealProjective4 line 21

    abbrev RealProjective4 := Projectivization ℝ (EuclideanSpace ℝ (Fin 5))

  • definition OAI.EinsteinFour.roundDistance line 23

    def roundDistance (p q : RoundSphere4) : ℝ :=  Real.arccos (inner ℝ p.val q.val)

  • definition OAI.EinsteinFour.fubiniStudyDistance line 26

    def fubiniStudyDistance (p q : ComplexProjective2) : ℝ :=  Real.arccos (‖inner ℂ p.rep q.rep‖ / (‖p.rep‖ * ‖q.rep‖))

  • definition OAI.EinsteinFour.realProjectiveDistance line 29

    def realProjectiveDistance (p q : RealProjective4) : ℝ :=  Real.arccos (‖inner ℝ p.rep q.rep‖ / (‖p.rep‖ * ‖q.rep‖))

  • abbreviation OAI.EinsteinFour.SmoothMetric line 37

    abbrev SmoothMetric :=  ContMDiffRiemannianMetric I4 ∞ FourSpace (TangentSpace I4 : M → Type _)

  • definition OAI.EinsteinFour.metricInChart line 42

    def metricInChart (g : SmoothMetric M) (c : M) (z : FourSpace) :    Matrix (Fin 4) (Fin 4) ℝ :=  let e := chartAt FourSpace c  let d := mfderiv I4 I4 e.symm z  fun i j => g.inner (e.symm z) (d (coordinateVector i)) (d (coordinateVector j))

  • definition OAI.EinsteinFour.partialDeriv line 48

    def partialDeriv (f : FourSpace → ℝ) (i : Fin 4) (z : FourSpace) : ℝ :=  fderiv ℝ f z (coordinateVector i)

  • definition OAI.EinsteinFour.christoffel line 51

    def christoffel (g : SmoothMetric M) (c : M) (z : FourSpace)    (k i j : Fin 4) : ℝ :=  (1 / 2 : ℝ) * ∑ l : Fin 4, (metricInChart g c z)⁻¹ k l *    (partialDeriv (fun w => metricInChart g c w j l) i z +     partialDeriv (fun w => metricInChart g c w i l) j z -     partialDeriv (fun w => metricInChart g c w i j) l z)

  • definition OAI.EinsteinFour.curvatureComponent line 58

    def curvatureComponent (g : SmoothMetric M) (c : M) (z : FourSpace)    (l i j k : Fin 4) : ℝ :=  partialDeriv (fun w => christoffel g c w l j k) i z -  partialDeriv (fun w => christoffel g c w l i k) j z +  ∑ p : Fin 4,    (christoffel g c z l i p * christoffel g c z p j k -     christoffel g c z l j p * christoffel g c z p i k)

  • definition OAI.EinsteinFour.ricciInChart line 66

    def ricciInChart (g : SmoothMetric M) (c : M) (z : FourSpace)    (i j : Fin 4) : ℝ :=  ∑ k : Fin 4, curvatureComponent g c z k k i j

  • definition OAI.EinsteinFour.sectionalNumerator line 70

    def sectionalNumerator (g : SmoothMetric M) (c : M) (z : FourSpace)    (u v : FourSpace) : ℝ :=  ∑ l : Fin 4, ∑ m : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4, ∑ k : Fin 4,    metricInChart g c z l m * curvatureComponent g c z l i j k *      u i * v j * v k * u m

  • definition OAI.EinsteinFour.IsEinstein line 76

    def IsEinstein (g : SmoothMetric M) : Prop :=  ∃ lam : ℝ, ∀ (c : M) (i j : Fin 4),    ricciInChart g c (chartAt FourSpace c c) i j =      lam * metricInChart g c (chartAt FourSpace c c) i j

  • definition OAI.EinsteinFour.HasPositiveSectionalCurvature line 81

    def HasPositiveSectionalCurvature (g : SmoothMetric M) : Prop :=  ∀ (c : M) (u v : FourSpace), LinearIndependent ℝ ![u, v] →    0 < sectionalNumerator g c (chartAt FourSpace c c) u v

  • definition OAI.EinsteinFour.scaledEDistance line 85

    def scaledEDistance (g : SmoothMetric M) (a : ℝ) (x y : M) : ℝ≥0∞ :=  letI : RiemannianBundle (TangentSpace I4 : M → Type _) := ⟨g.toRiemannianMetric⟩  ENNReal.ofReal (Real.sqrt a) * Manifold.riemannianEDist I4 x y

  • definition OAI.EinsteinFour.ScaledIsometricTo line 89

    def ScaledIsometricTo {N : Type*} (g : SmoothMetric M) (a : ℝ)    (modelDistance : N → N → ℝ) : Prop :=  ∃ f : M ≃ N, ∀ x y : M,    ENNReal.ofReal (modelDistance (f x) (f y)) = scaledEDistance g a x y

  • abbreviation OAI.PositiveEinsteinFour.Geometry.Mat4 line 107

    abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ

  • definition OAI.PositiveEinsteinFour.Geometry.chartMetric line 109

    def chartMetric (g : SmoothMetric M) (c : M) : Mat4 :=  metricInChart g c (chartAt FourSpace c c)

  • structure OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame line 112

    structure OrthonormalFrame (g : SmoothMetric M) (c : M) where  matrix : Mat4  orthonormal : matrixᵀ * chartMetric g c * matrix = 1

  • structure OAI.PositiveEinsteinFour.Geometry.FrameBundle line 125

    structure FrameBundle (g : SmoothMetric M) where  base : M  frame : OrthonormalFrame g base

4 more definitions are reached the same way; the full file lists them.

Possible paper match, with no recorded review

No paper statement clearly matched the Lean wording. Statement Map, the program that collects Atlas’s source records, selected this possible match using words in OpenAI’s catalogue and Lean note. No review of whether the statements mean the same thing is recorded.

Shared with the catalogue’s wording or OpenAI’s note, none of them matched in the Lean text: closed, connected, curvature, einstein, four, fubini, manifold, metric and eight more.

Statements in Positively curved Einstein four-manifolds come first because the release lists only that paper for this Lean statement.

Theorem 1.1 of Positively curved Einstein four-manifolds

Theorem

Let (M,g) be a connected smooth closed Einstein four-manifold with strictly positive sectional curvature, without an orientability assumption. There is a constant a>0 such that (M,ag) is isometric to the standard round S^4, to \mathbb{CP}^2 with its Fubini–Study metric, or to \mathbb{RP}^4 with its standard round metric.

Section 1, Introduction Read it in the paper TeX source, line 13
Show the TeX
Let $(M,g)$ be a connected smooth closed Einstein four-manifold with
strictly positive sectional curvature, without an orientability
assumption. There is a constant $a>0$ such that $(M,ag)$ is isometric to
the standard round $S^4$, to $\mathbb{CP}^2$ with its Fubini--Study
metric, or to $\mathbb{RP}^4$ with its standard round metric.

Other possible paper matches, closest wording first

  • Corollary 8.9 of Positively curved Einstein four-manifolds. Words of the Lean statement, its names split into words, that also appear in the theorem: classification, scaling, einstein, complex, positive, isometric and twelve more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: strictly.
  • Corollary 1.2 of Zero-Plane Rigidity for Einstein Four-Manifolds. Words of the Lean statement, its names split into words, that also appear in the theorem: projective, sqrt, complex, riemannian, fubini, study and eight more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: plane.
  • Classification Assumption 1.1 of An L² Einstein Gap for Nonnegatively Curved Four-Manifolds. Words of the Lean statement, its names split into words, that also appear in the theorem: sqrt, isometric, riemannian, fubini, study, round and nine more.
  • Theorem 1.1 of Zero-Plane Rigidity for Einstein Four-Manifolds. Words of the Lean statement, its names split into words, that also appear in the theorem: tangent, sqrt, bundle, isometric, riemannian, smooth and five more. Found in the paper’s title, which its main theorem states: einstein and four. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: plane.
  • Theorem 1.2 of An L² Einstein Gap for Nonnegatively Curved Four-Manifolds. Words of the Lean statement, its names split into words, that also appear in the theorem: scal, classification, standard, riemannian, orientation, smooth and four more.
  • Proposition 7.1 of Zero-Plane Rigidity for Einstein Four-Manifolds. Words of the Lean statement, its names split into words, that also appear in the theorem: sectional, oriented, curvature, four, one, manifold and two more.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

One independent group reports that Comparator accepted a run for this Lean statement file: Carlos Toledo’s cert-machine. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

  • Accepted Their term: “CERTIFIED”.

    Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.

    Reported 10 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 348’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

  • MathVet

    Finds part of it stated, or a narrower or weaker statement Their term: “partial”.

    Only a special case is stated, or a co-equal headline claim has no challenge statement. Their record

    Their note: The Lean classification assumes strictly positive sectional curvature (HasPositiveSectionalCurvature) and concludes scaled isometry to round S⁴, Fubini-Study ℂP² or round ℝP⁴ (oriented case: S⁴ or ℂP²). That is a special case of the summary's nonnegative-curvature classification (which also has the S²×S² product); the L² trace-free-Ricci topological gap theorem is not stated.

    Definitions the group asks readers to compare with the paper: Curvature is computed by hand in the centre chart of each point (christoffel, curvatureComponent, ricciInChart, sectionalNumerator, IsEinstein := ∃ lam, ricci = lam·g at chartAt c c), and model spaces are only given as distance functions (roundDistance := arccos ⟨p,q⟩, fubiniStudyDistance := arccos(‖⟨p,q⟩‖/(‖p‖‖q‖)), realProjectiveDistance) compared to Manifold.riemannianEDist scaled by √a (ScaledIsometricTo); two statement-level run_cmd Lean.modifyEnv ... auxLemmasExt meta commands; external package RellichKondrachov in the solution cone

  • Carlos Toledo’s cert-machine

    Finds part of it stated, or a narrower or weaker statement Their term: “NARROWER — UNLINKED”.

    The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link. Their record

    Their note: The nonnegative-curvature classification (zero-plane rigidity: universal cover S²×S² with equal radii) and the L² trace-free-Ricci gap theorem — the two October manuscripts, neither linked by the scope note.

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“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.”

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

222 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 135 to its own declarations, 102 to Mathlib’s documentation. 32 declared names also link to the same declaration in OpenAI’s library. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAInoncomputable sectionopen scoped Manifold ContDiff BigOperators ENNRealopen Bundlenamespace EinsteinFourabbrev FourSpace := EuclideanSpace ℝ (Fin 4)abbrev I4 := 𝓘(ℝ, FourSpace)def coordinateVector (i : Fin 4) : FourSpace := EuclideanSpace.single i 1abbrev RoundSphere4 := {x : EuclideanSpace ℝ (Fin 5) // ‖x‖ = 1}abbrev ComplexProjective2 := Projectivization ℂ (EuclideanSpace ℂ (Fin 3))abbrev RealProjective4 := Projectivization ℝ (EuclideanSpace ℝ (Fin 5))def roundDistance (p q : RoundSphere4) : ℝ :=  Real.arccos (inner ℝ p.val q.val)def fubiniStudyDistance (p q : ComplexProjective2) : ℝ :=  Real.arccos (‖inner ℂ p.rep q.rep‖ / (‖p.rep‖ * ‖q.rep‖))def realProjectiveDistance (p q : RealProjective4) : ℝ :=  Real.arccos (‖inner ℝ p.rep q.rep‖ / (‖p.rep‖ * ‖q.rep‖))section Metricvariable (M : Type*) [TopologicalSpace M] [ChartedSpace FourSpace M]  [IsManifold I4 ∞ M]abbrev SmoothMetric :=  ContMDiffRiemannianMetric I4 ∞ FourSpace (TangentSpace I4 : M → Type _)variable {M}def metricInChart (g : SmoothMetric M) (c : M) (z : FourSpace) :    Matrix (Fin 4) (Fin 4) ℝ :=  let e := chartAt FourSpace c  let d := mfderiv I4 I4 e.symm z  fun i j => g.inner (e.symm z) (d (coordinateVector i)) (d (coordinateVector j))def partialDeriv (f : FourSpace → ℝ) (i : Fin 4) (z : FourSpace) : ℝ :=  fderiv ℝ f z (coordinateVector i)def christoffel (g : SmoothMetric M) (c : M) (z : FourSpace)    (k i j : Fin 4) : ℝ :=  (1 / 2 : ℝ) * ∑ l : Fin 4, (metricInChart g c z)⁻¹ k l *    (partialDeriv (fun w => metricInChart g c w j l) i z +     partialDeriv (fun w => metricInChart g c w i l) j z -     partialDeriv (fun w => metricInChart g c w i j) l z)def curvatureComponent (g : SmoothMetric M) (c : M) (z : FourSpace)    (l i j k : Fin 4) : ℝ :=  partialDeriv (fun w => christoffel g c w l j k) i z -  partialDeriv (fun w => christoffel g c w l i k) j z +  ∑ p : Fin 4,    (christoffel g c z l i p * christoffel g c z p j k -     christoffel g c z l j p * christoffel g c z p i k)def ricciInChart (g : SmoothMetric M) (c : M) (z : FourSpace)    (i j : Fin 4) : ℝ :=  ∑ k : Fin 4, curvatureComponent g c z k k i jdef sectionalNumerator (g : SmoothMetric M) (c : M) (z : FourSpace)    (u v : FourSpace) : ℝ :=  ∑ l : Fin 4, ∑ m : Fin 4, ∑ i : Fin 4, ∑ j : Fin 4, ∑ k : Fin 4,    metricInChart g c z l m * curvatureComponent g c z l i j k *      u i * v j * v k * u mdef IsEinstein (g : SmoothMetric M) : Prop :=  ∃ lam : ℝ, ∀ (c : M) (i j : Fin 4),    ricciInChart g c (chartAt FourSpace c c) i j =      lam * metricInChart g c (chartAt FourSpace c c) i jdef HasPositiveSectionalCurvature (g : SmoothMetric M) : Prop :=  ∀ (c : M) (u v : FourSpace), LinearIndependent ℝ ![u, v] →    0 < sectionalNumerator g c (chartAt FourSpace c c) u vdef scaledEDistance (g : SmoothMetric M) (a : ℝ) (x y : M) : ℝ≥0∞ :=  letI : RiemannianBundle (TangentSpace I4 : M → Type _) := ⟨g.toRiemannianMetric⟩  ENNReal.ofReal (Real.sqrt a) * Manifold.riemannianEDist I4 x ydef ScaledIsometricTo {N : Type*} (g : SmoothMetric M) (a : ℝ)    (modelDistance : N → N → ℝ) : Prop :=  ∃ f : M ≃ N, ∀ x y : M,    ENNReal.ofReal (modelDistance (f x) (f y)) = scaledEDistance g a x yend Metricend EinsteinFourrun_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.modifyState env fun _ => {}namespace PositiveEinsteinFour.Geometryopen EinsteinFour Matrixvariable {M : Type*} [TopologicalSpace M] [ChartedSpace FourSpace M]  [IsManifold I4 ∞ M]abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝdef chartMetric (g : SmoothMetric M) (c : M) : Mat4 :=  metricInChart g c (chartAt FourSpace c c)structure OrthonormalFrame (g : SmoothMetric M) (c : M) where  matrix : Mat4  orthonormal : matrixᵀ * chartMetric g c * matrix = 1def OrthonormalFrame.map {g : SmoothMetric M} {c : M} (e : OrthonormalFrame g c) :    FourSpace →ₗ[ℝ] FourSpace :=  (WithLp.linearEquiv 2 ℝ (Fin 4 → ℝ)).symm.toLinearMap ∘ₗ    (Matrix.mulVecLin e.matrix) ∘ₗ (WithLp.linearEquiv 2 ℝ (Fin 4 → ℝ)).toLinearMapdef OrthonormalFrame.vector {g : SmoothMetric M} {c : M}    (e : OrthonormalFrame g c) (i : Fin 4) : FourSpace :=  WithLp.toLp 2 (fun a => e.matrix a i)structure FrameBundle (g : SmoothMetric M) where  base : M  frame : OrthonormalFrame g basedef frameRealization {g : SmoothMetric M} (e : FrameBundle g) :    M × (Fin 4 → TangentBundle I4 M) :=  (e.base, fun i => ⟨e.base, e.frame.vector i⟩)run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.modifyState env fun _ => {}instance (g : SmoothMetric M) : TopologicalSpace (FrameBundle g) :=  TopologicalSpace.induced frameRealization inferInstance/-- An orientation is a clopen choice of determinant sign in every frame fiber. -/structure FrameOrientation (g : SmoothMetric M) where  positive : Set (FrameBundle g)  clopen : IsClopen positive  nonempty_fiber : ∀ c, ∃ e : OrthonormalFrame g c, (⟨c, e⟩ : FrameBundle g) ∈ positive  compatible : ∀ c (e f : OrthonormalFrame g c),    (⟨c, e⟩ : FrameBundle g) ∈ positive →      ((⟨c, f⟩ : FrameBundle g) ∈ positive ↔ 0 < e.matrix.det * f.matrix.det)end PositiveEinsteinFour.Geometrynamespace PositiveEinsteinFouropen EinsteinFouruniverse u/-- A connected closed oriented smooth Riemannian four-manifold. -/structure ClosedOrientedMetricFour where  manifold : ModelWithCorners.MfldCat.{u} I4 ∞  [regular : T3Space manifold]  [secondCountable : SecondCountableTopology manifold]  [compact : CompactSpace manifold]  [connected : ConnectedSpace manifold]  metric : SmoothMetric manifold  orientation : Geometry.FrameOrientation metricattribute [instance] ClosedOrientedMetricFour.regular  ClosedOrientedMetricFour.secondCountable ClosedOrientedMetricFour.compact  ClosedOrientedMetricFour.connectedsection ClassificationDefinitionsvariable {M : Type*} [TopologicalSpace M] [ChartedSpace FourSpace M]  [IsManifold I4 ∞ M]/-- Positive rescaling identifies the metric with one of the three standard models. -/def Classified (g : SmoothMetric M) : Prop :=  ∃ a : ℝ, 0 < a ∧    (ScaledIsometricTo g a roundDistance ∨      ScaledIsometricTo g a fubiniStudyDistance ∨      ScaledIsometricTo g a realProjectiveDistance)def ClassificationOn (M : Type*) [TopologicalSpace M] [ChartedSpace FourSpace M]    [IsManifold I4 ∞ M] [T2Space M] [SecondCountableTopology M]    [CompactSpace M] [ConnectedSpace M] : Prop :=  ∀ g : SmoothMetric M,    IsEinstein g → HasPositiveSectionalCurvature g → Classified gend ClassificationDefinitions/-- The oriented classification has the round sphere and Fubini--Study models. -/theorem orientedClassification (X : ClosedOrientedMetricFour.{u})    (hEinstein : IsEinstein X.metric) (hpositive : HasPositiveSectionalCurvature X.metric) :    ∃ a : ℝ, 0 < a ∧ (ScaledIsometricTo X.metric a roundDistance ∨      ScaledIsometricTo X.metric a fubiniStudyDistance) := by  sorrysectionvariable (M : Type u) [TopologicalSpace M] [ChartedSpace FourSpace M]  [IsManifold I4 ∞ M] [T2Space M] [SecondCountableTopology M]  [CompactSpace M] [ConnectedSpace M]theorem classificationOn : ClassificationOn M := by  sorryend/-- The connected closed classification includes the real projective quotient. -/theorem classification (M : Type*) [TopologicalSpace M] [ChartedSpace FourSpace M]    [IsManifold I4 ∞ M] [T2Space M] [SecondCountableTopology M]    [CompactSpace M] [ConnectedSpace M] (g : SmoothMetric M)    (hEinstein : IsEinstein g) (hpositive : HasPositiveSectionalCurvature g) :    ∃ a : ℝ, 0 < a ∧      (ScaledIsometricTo g a roundDistance ∨        ScaledIsometricTo g a fubiniStudyDistance ∨        ScaledIsometricTo g a realProjectiveDistance) := by  sorryend PositiveEinsteinFourendend OAI
Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Positively curved Einstein four-manifolds

Theorem

Let (M,g) be a connected smooth closed Einstein four-manifold with strictly positive sectional curvature, without an orientability assumption. There is a constant a>0 such that (M,ag) is isometric to the standard round S^4, to \mathbb{CP}^2 with its Fubini–Study metric, or to \mathbb{RP}^4 with its standard round metric.

Section 1, Introduction Read it in the paper TeX source, line 13
Show the TeX
Let $(M,g)$ be a connected smooth closed Einstein four-manifold with
strictly positive sectional curvature, without an orientability
assumption. There is a constant $a>0$ such that $(M,ag)$ is isometric to
the standard round $S^4$, to $\mathbb{CP}^2$ with its Fubini--Study
metric, or to $\mathbb{RP}^4$ with its standard round metric.
Configuration and file facts
OpenAI’s Lean catalogue
OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 348 link it.
Solution module
OAI.Geometry.EinsteinFour.Classification
Allowed axioms
propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports
Mathlib
Imports from outside Mathlib
None
Local vocabulary
32 local vocabulary declarations
Lines of Lean, without comments or blank lines
128
Second proof-verification program (nanoda)
Off in OpenAI's configuration.

Statement comparison

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas

Classification of positively curved Einstein four-manifolds

Family 348: Nonnegative-curvature Einstein classification and an L2 topological gap

Candidate pairing

Theorem

Let (M,g) be a connected smooth closed Einstein four-manifold with strictly positive sectional curvature, without an orientability assumption. There is a constant a>0 such that (M,ag) is isometric to the standard round S^4, to \mathbb{CP}^2 with its Fubini–Study metric, or to \mathbb{RP}^4 with its standard round metric.

Positively curved Einstein four-manifolds

TeX label thm:classification, build/sections/01-introduction.tex, line 13

The Lean statement says

theorem orientedClassification (X : ClosedOrientedMetricFour.{u})    (hEinstein : IsEinstein X.metric) (hpositive : HasPositiveSectionalCurvature X.metric) :    ∃ a : ℝ, 0 < a ∧ (ScaledIsometricTo X.metric a roundDistance ∨      ScaledIsometricTo X.metric a fubiniStudyDistance) := by  sorrytheorem classificationOn : ClassificationOn M := by  sorrytheorem classification (M : Type*) [TopologicalSpace M] [ChartedSpace FourSpace M]    [IsManifold I4 ∞ M] [T2Space M] [SecondCountableTopology M]    [CompactSpace M] [ConnectedSpace M] (g : SmoothMetric M)    (hEinstein : IsEinstein g) (hpositive : HasPositiveSectionalCurvature g) :    ∃ a : ℝ, 0 < a ∧      (ScaledIsometricTo g a roundDistance ∨        ScaledIsometricTo g a fubiniStudyDistance ∨        ScaledIsometricTo g a realProjectiveDistance) := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Atlas selected this possible match because the two statements share words. No review of whether they mean the same thing is recorded.One independent group reports that Comparator accepted a run for this file at the release version shown here.Statement review: none recorded

32 local vocabulary declarationsAllowed axioms: propext, Quot.sound, Classical.choiceopenai/math at fd4aeebwcook04.github.io/plectis-atlas/statements/EinsteinFour.html

Recorded comparisons with the paper

Atlas records no contributed comparison of this statement with the paper.

Contributed Comparator run reports

Atlas records no contributed report of running Comparator for this statement file.

Questions to resolve when comparing this statement with the paper

  • Both independent readers find this family's challenges state less than its headline, while the atlas's AI draft classes this file as stating a paper's theorem as the paper does; check which part of the headline it covers.

Compare this statement with the paperShare a Comparator run reportSuggest a change