openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance
← Problems

Topology · Geometry · Theorem

Poincaré conjecture

Is every closed, simply connected three-dimensional manifold homeomorphic to the three-sphere?

ProvedOpenMath assessment · Oct 12, 2026
Cite & export
Open this versionExport record · JSONRecord detailsReport a correction
Use with an agent

Earlier version 5 of this page. View current →

Overview

Known

The three-dimensional theorem is proved by Perelman’s work, with detailed proof accounts. Recent sources also report complete Lean formalizations; their exact statements and externally checked revisions are listed separately.

Latest

Precise statement

Closed means compact without boundary. Simply connected includes path connectedness and says every loop can be contracted to a point. The conclusion is a homeomorphism to the standard three-sphere, not an isometry for an arbitrary metric. This is the topological theorem in dimension three.

Background

How to read this question

What the theorem identifies

A closed simply connected three-manifold has the same topology as the three-sphere. The theorem does not require its chosen metric to be round.

Limit Having the sphere’s homology alone is weaker than being simply connected.

Sources & review

Supporting statements

Source-grounded explanation · independent explanation review: pending.

Question paraphrased by OpenMath. Original wording is available in the sources.

Results

The question 1

Equivalent formulations 1

Supporting results 1

Variants and analogues 2

  • Open
    The smooth four-dimensional Poincaré question

    This is a separate conjecture in dimension four; simple connectivity alone is insufficient for its hypothesis.

  • Proved
    The topological four-dimensional theorem

    Freedman’s topological conclusion does not identify a smooth structure or imply the smooth four-dimensional conjecture.

    Manolescu 2026

Background 1

Connections

How the recorded statements connect
relatedanalogueThe topological four-dimensional theorem · ProvedThe topologicalfour-dimensional theorem● ProvedThe topological three-dimensional Poincaré theorem · ProvedThe topologicalthree-dimensional Poincaré…● ProvedThe smooth four-dimensional Poincaré question · OpenThe smooth four-dimensionalPoincaré question○ Open
  • ━ ⇔ equivalent
  • → implies
  • ┅ analogue or related (no logical link)
  • Border colour = status
2 connections. Select a statement in the graph to show only its entries.

Analogues and related questions 2

Approaches

How the problem is attacked, and what each line of attack cannot yet reach.

Ricci flow, surgery and finite extinction

The accepted proof follows Hamilton’s geometric evolution, Perelman’s control of singularities and surgery, and finite extinction followed by topological reconstruction.

Cannot yet reach This is a reading guide to the cited proof, not a replacement for its analytic and topological arguments.

Sources & review

Supporting statements

Source-grounded explanation · independent explanation review: pending.

From a smooth proof to the topological theorem

Moise smoothing provides compatible smooth structure, the smooth theorem yields a diffeomorphism to the sphere, and forgetting smooth structure gives a homeomorphism.

Cannot yet reach The smoothing step is dimension-specific; the analogous smooth four-dimensional question remains open.

Sources & review

Supporting statements

Source-grounded explanation · independent explanation review: pending.

Timeline

  1. An AI-assisted formalization accountFormalization

    The preprint describes the project and public evidence.

    Historical mathematics, external formal reports and OpenMath verification are separate evidence.

  2. External comparator verification is reportedFormalization

    FrenzyMath records statement and kernel checks at its named proof commit.

    Historical mathematics, external formal reports and OpenMath verification are separate evidence.

  3. A source-pinned Lean formalization reportFormalization

    The authors report smooth and topological proofs with release-specific endpoint audits.

    Historical mathematics, external formal reports and OpenMath verification are separate evidence.

  4. A detailed proof accountRelated result

    Morgan and Tian publish the proof and three-sphere conclusion.

    Historical mathematics, external formal reports and OpenMath verification are separate evidence.

  5. Perelman’s finite-extinction argumentRelated result

    The final preprint supplies extinction for the relevant Ricci flows with surgery.

    Historical mathematics, external formal reports and OpenMath verification are separate evidence.

  6. Poincaré poses the questionFoundation

    The loop-contraction question becomes the three-dimensional conjecture.

    Historical mathematics, external formal reports and OpenMath verification are separate evidence.

Full history with sources →

Evidence

Literature

2 published papers · 3 preprints · 2 projects

Status OpenMath assessment · Oct 12, 2026.

  • Proved: Clay · Millennium Problems · Solved ↗ · source date not recorded · checked Oct 1, 2026The cited source item and version only; this is not an independent OpenMath assessment.
Formal

4 complete proofs

6 formalizations below ↓

Reported in sources: Complete Lean proofs of the topological and smooth three-dimensional statements are reported by two external projects. Links below pin the relevant source revisions. Mathlib’s wanted declarations remain statement-only at the inspected revision. No OpenMath proof build or independent correspondence review is recorded.

Computation

None recorded

Review

Not yet reviewed

OpenMath assessment: The three-dimensional theorem is proved by Perelman’s work, with detailed proof accounts. Recent sources also report complete Lean formalizations; their exact statements and externally checked revisions are listed separately.

The canonical question and cited source selection only.

OpenMath pilot collection · OpenMath source curation · assessed Oct 12, 2026 · review due Jan 12, 2027

Collection last checked Oct 12, 2026.

Formalizations

The topological three-dimensional Poincaré theorem →

Topological theorem · DifferentialGeometry release v0.1.3Complete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

The preprint reports a complete Lean proof of the exact topological theorem at this release. Endpoint source was inspected; OpenMath has not rebuilt its dependency closure or independently reviewed correspondence.

Statement match: Candidate correspondence · not independently confirmed · checked Oct 12, 2026

Declaration & revision
DifferentialGeometry.Topology.poincare_conjecture

Commit 7a48598d35109aa99d1cc678e2724c213cdf4ff3

Topological theorem · FrenzyMath reported verified revisionComplete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

Project evidence reports successful statement comparison and Lean/Nanoda verification for this proof commit. The later report revision is cited separately; OpenMath has not rerun these checks or completed independent mathematical review.

Statement match: Candidate correspondence · not independently confirmed · checked Oct 12, 2026

Declaration & revision
PoincareConjecture.ComparatorTargets.topologicalPoincareSkeleton

Commit 1876d7dc2c85325a3f62ce9776af98f910c5db04

Topological statement · Mathlib wanted theoremStatement only · proof not supplied in this source

Open formal source ↗

Statement only · proof not supplied in this source

This revision uses proof_wanted for the exact statement. A wanted declaration is not a completed Mathlib proof; the external projects above have separate source and verification evidence.

Statement match: Candidate correspondence · not independently confirmed · checked Oct 12, 2026

Declaration & revision
SimplyConnectedSpace.nonempty_homeomorph_sphere_three

Commit 9454a4c25a2b923eb55dba3098f2d6ae0484d09b

The smooth three-dimensional theorem →

Smooth theorem · DifferentialGeometry release v0.1.3Complete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

The preprint reports a complete Lean proof at this release. Its formal scope is the smooth three-dimensional theorem; OpenMath has not reproduced the build.

Statement match: Candidate correspondence · not independently confirmed · checked Oct 12, 2026

Declaration & revision
DifferentialGeometry.PDE.RicciFlow.Surgery.Topology.smoothPoincareConjecture_holds

Commit 7a48598d35109aa99d1cc678e2724c213cdf4ff3

Smooth theorem · FrenzyMath reported verified revisionComplete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

Project evidence reports successful statement comparison and Lean/Nanoda verification for this proof commit. The later report revision is cited separately; OpenMath has not rerun these checks or completed independent mathematical review.

Statement match: Candidate correspondence · not independently confirmed · checked Oct 12, 2026

Declaration & revision
PoincareConjecture.ComparatorTargets.smoothPoincareSkeleton

Commit 1876d7dc2c85325a3f62ce9776af98f910c5db04

Smooth statement · Mathlib wanted theoremStatement only · proof not supplied in this source

Open formal source ↗

Statement only · proof not supplied in this source

This revision uses proof_wanted for the exact statement. A wanted declaration is not a completed Mathlib proof; the external projects above have separate source and verification evidence.

Statement match: Candidate correspondence · not independently confirmed · checked Oct 12, 2026

Declaration & revision
SimplyConnectedSpace.nonempty_sdiffeomorph_sphere_three

Commit 9454a4c25a2b923eb55dba3098f2d6ae0484d09b

External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.

Sources

Choose a starting point below. Each result links to its exact statement, cited passages and checks.

Start here

Bibliography 9

Research activity · 1 entry

Contributions

Both formalization projects self-report automated assistance; this attribution is separate from theorem truth and verification evidence.

Formalization

Two public formalization projects

The selected 2026 projects report complete smooth and topological three-dimensional proofs, with exact release or verification revisions.

These source reports do not constitute OpenMath executions or independently reviewed mathematical correspondence.

Related statements · context, not additional proved progress

A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture · sources & artifacts →

An AI-Assisted Formalization of the Poincaré Conjecture · sources & artifacts →

Poincaré comparator integration verification · sources & artifacts →

Selected literature; source observations and coverage limits are retained in the publication details.

Record details
Record version
5
Classification
MSC2020 57K30 / 57R60
Prerequisite level
graduate
Source observations & version history →