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 13 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.

Definitions

Closed and simply connected
Closed means compact without boundary. Simply connected means path connected with every loop contractible; the question concerns three-dimensional manifolds.

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.

Landscape

Figures and explorable examples. Selecting a statement opens its exact wording.

Visual setup

Spheres in every dimension

The same question asked up to homeomorphism and up to diffeomorphism. Topologically the answer is yes in each dimension shown; smoothly it fails wherever exotic spheres exist, and is open in dimension four.

Reading boundary. Only dimensions 3–13 are drawn. Beyond them the cited source reports a standard smooth sphere also in dimension 61 and exotic spheres in every other dimension up to 63. Piecewise linear structures are not shown.

Dimension n

Homeomorphic to Sⁿ

Dimension n 3: Holds there.Perelman● Proved under stated assumptions
Dimension n 4: Holds there.Freedman● Proved under stated assumptions
Dimension n 5–13: Holds there.Smale: smooth homotopy spheres● Proved under stated assumptions

Diffeomorphic to Sⁿ

Dimension n 3: Holds there.Standard● Proved under stated assumptions
Dimension n 4: Open.Open○ Open
Dimension n 5–6: Holds there.Standard● Proved under stated assumptions
Dimension n 7–11: Fails there: counterexamples exist.Exotic spheres exist● Proved under stated assumptions
Dimension n 12: Holds there.Standard● Proved under stated assumptions
Dimension n 13: Fails there: counterexamples exist.Exotic● Proved under stated assumptions

✓ Holds there✗ Fails there: counterexamples exist? OpenEach cell links to its statement and status

Text version

Columns are dimensions 3 to 13. The upper track asks whether a manifold homotopy equivalent to Sⁿ is homeomorphic to it: Perelman in dimension three, Freedman in dimension four and Smale, for smooth homotopy spheres, from dimension five. The lower track asks whether a smooth manifold homeomorphic to Sⁿ is diffeomorphic to the standard Sⁿ: yes in dimensions 3, 5, 6 and 12, no in 7–11 and 13 because exotic spheres exist there, and unknown in dimension four.

Closed manifolds; homotopy equivalent to Sⁿ for the upper track, homeomorphic to Sⁿ for the lower track. From dimension five the upper track cites Smale’s theorem for smooth homotopy spheres only.

  1. Perelman

    Proved

    The topological three-dimensional Poincaré theorem

    Scope & assumptions. Compact Hausdorff three-manifolds without boundary; simply connected includes connectedness.

    The topological three-dimensional Poincaré theorem →

  2. Freedman

    Proved

    The topological four-dimensional theorem

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

    The topological four-dimensional theorem →

  3. Smale: smooth homotopy spheres

    Proved

    The Poincaré theorem in dimensions five and higher (Smale)

    The conclusion is a homeomorphism to Sⁿ. The smooth conclusion is a diffeomorphism to two balls glued along their boundaries, not necessarily to Sⁿ.

    The Poincaré theorem in dimensions five and higher (Smale) →

  4. Standard

    Proved

    The smooth three-dimensional theorem

    Scope & assumptions. Smoothness is additional structure; in dimension three the classification agrees with the topological theorem via smoothing and uniqueness of smooth structures.

    The smooth three-dimensional theorem →

  5. Open

    Open

    The smooth four-dimensional Poincaré question

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

    The smooth four-dimensional Poincaré question →

  6. Standard

    Proved

    Dimensions where every smooth sphere is standard

    The source states that the group of oriented diffeomorphism classes of manifolds homeomorphic to Sⁿ is trivial for these n. Dimension four is excluded: there the question is open.

    Dimensions where every smooth sphere is standard →

  7. Exotic spheres exist

    Proved

    Exotic spheres in every other dimension up to 63

    The source states that the group of oriented diffeomorphism classes is non-trivial for these n. Since Sⁿ has an orientation-reversing diffeomorphism, a non-trivial class is not diffeomorphic to Sⁿ at all. The smooth Poincaré statement therefore fails in these dimensions.

    Exotic spheres in every other dimension up to 63 →

  8. Standard

    Proved

    Dimensions where every smooth sphere is standard

    The source states that the group of oriented diffeomorphism classes of manifolds homeomorphic to Sⁿ is trivial for these n. Dimension four is excluded: there the question is open.

    Dimensions where every smooth sphere is standard →

  9. Exotic

    Proved

    Exotic spheres in every other dimension up to 63

    The source states that the group of oriented diffeomorphism classes is non-trivial for these n. Since Sⁿ has an orientation-reversing diffeomorphism, a non-trivial class is not diffeomorphic to Sⁿ at all. The smooth Poincaré statement therefore fails in these dimensions.

    Exotic spheres in every other dimension up to 63 →

Sources & review

Authored by OpenMath curation on 2026-10-21 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

Visual setup

How the three-dimensional case was proved

Perelman’s Ricci flow with surgery proves the smooth statement; Moise’s smoothing theorem transfers it to topological manifolds. Select a step to read the exact statement.

Reading boundary. An outline only. The detailed proofs are in Perelman’s papers and the Morgan–Tian account, and the step from finite extinction to the smooth sphere needs further arguments not drawn here.

  1. Finite extinction● Proved under stated assumptions

    Ricci flow with surgery on a simply connected closed smooth three-manifold becomes extinct in finite time.

  2. Smooth three-sphere● Proved under stated assumptions

    Hence every closed, simply connected smooth three-manifold is diffeomorphic to the standard three-sphere.

  3. Moise smoothing● Proved under stated assumptions

    Every closed topological three-manifold admits a compatible smooth structure.

  4. Topological three-sphere● Proved under stated assumptions

    So every closed, simply connected topological three-manifold is homeomorphic to the three-sphere.

Text version

Start with a smooth simply connected closed three-manifold and any Riemannian metric. Ricci flow with surgery becomes extinct in finite time, which identifies the manifold with the smooth three-sphere. Every topological three-manifold admits a smooth structure (Moise), so the topological statement follows.

Closed, simply connected three-manifolds. Each step is a cited statement; the arrows show how the proof uses them, not a formal derivation.

  1. Finite extinction

    Proved

    Finite extinction in the simply connected case

    Scope & assumptions. Extinction concerns the flow with surgery, including discarded components; it does not mean that the original manifold vanishes under a homeomorphism.

    Finite extinction in the simply connected case →

  2. Smooth three-sphere

    Proved

    The smooth three-dimensional theorem

    Scope & assumptions. Smoothness is additional structure; in dimension three the classification agrees with the topological theorem via smoothing and uniqueness of smooth structures.

    The smooth three-dimensional theorem →

  3. Moise smoothing

    Proved

    Smoothing a topological three-manifold

    Scope & assumptions. This existence statement supplies the smooth input for the topological theorem; it alone does not classify the manifold.

    Smoothing a topological three-manifold →

  4. Topological three-sphere

    Proved

    The topological three-dimensional Poincaré theorem

    Scope & assumptions. Compact Hausdorff three-manifolds without boundary; simply connected includes connectedness.

    The topological three-dimensional Poincaré theorem →

Sources & review

Authored by OpenMath curation on 2026-10-21 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

Results

The question 1

Equivalent formulations 1

Supporting results 1

Variants and analogues 5

  • 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
  • Proved
    The Poincaré theorem in dimensions five and higher (Smale)

    The conclusion is a homeomorphism to Sⁿ. The smooth conclusion is a diffeomorphism to two balls glued along their boundaries, not necessarily to Sⁿ.

    per Milnor (official description)
  • Proved
    Dimensions where every smooth sphere is standard

    The source states that the group of oriented diffeomorphism classes of manifolds homeomorphic to Sⁿ is trivial for these n.

    Milnor 2014
  • Proved
    Exotic spheres in every other dimension up to 63

    The source states that the group of oriented diffeomorphism classes is non-trivial for these n.

    Milnor 2014

Background 1

Compare statements · 4

Each row is a separate assertion. Its assumptions determine which question it answers.

Statement scopes and hypotheses
StatementDimensionCategory
The topological three-dimensional Poincaré theorem →

Proved

Exact statement & sources		3Topological · homeomorphism
The smooth three-dimensional theorem →

Proved

Exact statement & sources		3Smooth · diffeomorphism
The smooth four-dimensional Poincaré question →

Open

Exact statement & sources		4Smooth · diffeomorphism
The topological four-dimensional theorem →

Proved

Exact statement & sources		4Topological · homeomorphism

Connections

How the recorded statements connect
relatedanalogueTopological Poincaré in dimension 4 · ProvedTopological Poincaré indimension 4● ProvedTopological Poincaré in dimension 3 · ProvedTopological Poincaré indimension 3● ProvedSmooth Poincaré in dimension 4 · OpenSmooth Poincaré in dimension 4○ 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.

  7. Verification date distinguished from publication dateSource correction

    The project report records checks on 28 September 2026. Its publication date is not established, and that verification event is not used as a bibliographic date.

    This metadata correction changes no mathematical statement, tested proof commit or externally reported check outcome.

Full history with sources →

Evidence

Literature

3 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 11

Research activity · 1 entry

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.

Contributors

Grigori Perelman proved the three-dimensional conjecture through Ricci flow, building on Richard Hamilton’s program. The two linked formalization projects self-report automated assistance; their 2026 work formalizes an established theorem.

Authors & roles

These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.

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