Proved
Solved ↗
The cited source item and version only; this is not an independent OpenMath assessment.
Clay · Millennium Problems · https://www.claymath.org/millennium/poincare-conjecture/ →
Observed Oct 1, 2026
Theorem · version 2
The topological three-dimensional Poincaré theorem
Statement
Every closed, simply connected topological three-manifold is homeomorphic to the standard three-sphere.
Assumptions
- Compact Hausdorff three-manifolds without boundary; simply connected includes connectedness.
- Dimension
- 3
- Category
- Topological · homeomorphism
- Clay · Millennium Problems →
- Ricci Flow and the Poincaré Conjecture →
- A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture →
- An AI-Assisted Formalization of the Poincaré Conjecture →
- Poincaré comparator integration verification →
- Mathlib · wanted Poincaré statements →
Evidence
Source reports
Formal proofs
Topological theorem · DifferentialGeometry release v0.1.3 ↗
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_conjectureCommit 7a48598d35109aa99d1cc678e2724c213cdf4ff3
Topological theorem · FrenzyMath reported verified revision ↗
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.topologicalPoincareSkeletonCommit 1876d7dc2c85325a3f62ce9776af98f910c5db04
Topological statement · Mathlib wanted theorem ↗
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_threeCommit 9454a4c25a2b923eb55dba3098f2d6ae0484d09b
Connections
In this problem · publication v13
Poincaré conjecture →
Primary formulation · Proved
Analogue
analogous toThe smooth four-dimensional Poincaré question
The four-dimensional smooth question concerns a different dimension and equivalence notion.
The three-dimensional theorem is fully proved; this analogue is not an unresolved part of it.
Details & sources
The topological three-dimensional Poincaré theorem →
Proved · version 2
Every closed, simply connected topological three-manifold is homeomorphic to the standard three-sphere.
- Compact Hausdorff three-manifolds without boundary; simply connected includes connectedness.
Scope: Compact Hausdorff three-manifolds without boundary; simply connected includes connectedness.
- Clay · Millennium Problems →
- Ricci Flow and the Poincaré Conjecture →
- A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture →
- An AI-Assisted Formalization of the Poincaré Conjecture →
- Poincaré comparator integration verification →
- Mathlib · wanted Poincaré statements →
The smooth four-dimensional Poincaré question →
Open · version 1
Every closed smooth four-manifold homotopy equivalent to the four-sphere is diffeomorphic to the standard smooth four-sphere.
- This is a separate conjecture in dimension four; simple connectivity alone is insufficient for its hypothesis.
Scope: This is a separate conjecture in dimension four; simple connectivity alone is insufficient for its hypothesis.
Relationship not independently reviewed.
Connection in Poincaré conjecture →Relationship not independently reviewed. This concerns its use in this problem.
Sources
A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture →
- §1, Theorems 1–3; §3, release and verification → · Original passage ↗
Recorded wording
The authors report Lean proofs of the smooth theorem and Moise smoothing, yielding the topological theorem. Their release v0.1.3 report names commit 7a48598d35109aa99d1cc678e2724c213cdf4ff3 and audits the endpoint closures for the three standard Lean axioms, without sorryAx or project axioms.
paraphrase · Follow the original source for authoritative statements and reuse terms.
Ziyang Qin · Yuan Liao · Ayush Khaitan · Bennett Chow · Preprint · Publication date Sep 27, 2026
Source-backed selection; publication and proof assessment are separate.
Revision & attribution
Source revision: arxiv-2609.33842v1. Observed Oct 12, 2026.
Authors report automated assistance; OpenMath has not independently assessed that workflow.
An AI-Assisted Formalization of the Poincaré Conjecture →
- Formal theorem endpoints and verification discussion → · Original passage ↗
Recorded wording
The team reports an AI-assisted Lean formalization of both the smooth and topological three-dimensional theorem, with public verification resources.
paraphrase · Follow the original source for authoritative statements and reuse terms.
Zhiyuan Zhang · Axel Delaval · Leheng Chen · Jinxuan Chen · Jie Xu · Yuxuan Liao · Jiedong Jiang · Chunlei Liu · Bin Dong · Preprint · Publication date Oct 6, 2026
Source-backed selection; publication and proof assessment are separate.
Revision & attribution
Source revision: arxiv-2610.08329v1. Observed Oct 12, 2026.
Authors report automated assistance; OpenMath has not independently assessed that workflow.
Clay · Millennium Problems →
- https://www.claymath.org/millennium/poincare-conjecture/ → · Original passage ↗
Recorded wording
Is every closed, simply connected three-dimensional manifold homeomorphic to the three-sphere?
paraphrase · Store metadata and original OpenMath paraphrases; follow the original source for authoritative wording.
Clay Mathematics Institute · Revision observed-2026-10-01
Mathlib · wanted Poincaré statements →
- SimplyConnectedSpace.nonempty_homeomorph_sphere_three and nonempty_sdiffeomorph_sphere_three → · Original passage ↗
Recorded wording
This Mathlib revision declares the three-dimensional topological and smooth Poincaré statements with proof_wanted. These are formal statements seeking library proofs, not evidence of a completed proof in Mathlib.
paraphrase · Follow the original source for authoritative statements and reuse terms.
Mathlib contributors · Project documentation
Source-backed selection; publication and proof assessment are separate.
Revision & attribution
Source revision: 9454a4c25a2b923eb55dba3098f2d6ae0484d09b. Observed Oct 12, 2026.
AI use is not reported in the selected source.
Poincaré comparator integration verification →
- Local integration verification; verification.json beside README → · Original passage ↗
Recorded wording
The project’s report records successful statement comparison and Lean/Nanoda checks on 28 September 2026 for proof commit 1876d7dc2c85325a3f62ce9776af98f910c5db04, permitting only the three standard axioms. Later documentation and import commits are not the tested revision; the report is project-supplied evidence.
paraphrase · Follow the original source for authoritative statements and reuse terms.
FrenzyMath contributors · Project documentation
Project-supplied verification report at the pinned documentation revision. The 28 September date describes verification, not publication; publication date is not established.
Revision & attribution
Source revision: 432c38f2aa5a30efb13871292d17b4a3309a496a; bibliographic metadata corrected 2026-10-12. Observed Oct 12, 2026.
Authors report automated assistance; OpenMath has not independently assessed that workflow.
Ricci Flow and the Poincaré Conjecture →
- Clay monograph 3; introduction, Theorem 0.1 and Corollary 0.2 → · Original passage ↗
Recorded wording
Morgan and Tian give a detailed proof of Perelman’s result, using Ricci flow with surgery and finite-time extinction to obtain the three-sphere conclusion.
paraphrase · Follow the original source for authoritative statements and reuse terms.
John Morgan · Gang Tian · Published · Publication date 2007
Source-backed selection; publication and proof assessment are separate.
Revision & attribution
Source revision: clay-monograph-3-2007. Observed Oct 12, 2026.
AI use is not reported in the selected source.
The Poincaré Conjecture · official description →
- §§1–3; dimension-three comparison on page 5 → · Original passage ↗
Recorded wording
Milnor distinguishes topological from smooth classification and explains why the distinctions disappear in dimension three. A homology sphere alone does not satisfy the Poincaré hypothesis.
paraphrase · Follow the original source for authoritative statements and reuse terms.
John Milnor · Published
Source-backed selection; publication and proof assessment are separate.
Revision & attribution
Source revision: clay-description-observed-2026-10-12. Observed Oct 12, 2026.
AI use is not reported in the selected source.
From Knots to Four-Manifolds →
- §3, Conjecture 3.1 and preceding topological classification → · Original passage ↗
Recorded wording
The survey states the smooth four-dimensional Poincaré conjecture as an open question, distinct from Freedman’s topological four-dimensional result.
paraphrase · Follow the original source for authoritative statements and reuse terms.
Ciprian Manolescu · Published · Publication date 2026
Source-backed selection; publication and proof assessment are separate.
Revision & attribution
Source revision: icm-2026-doi-25M1806703. Observed Oct 12, 2026.
AI use is not reported in the selected source.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Solved ↗
The cited source item and version only; this is not an independent OpenMath assessment.
Observed Oct 1, 2026 · Source passage →
Source updates
Verification date distinguished from publication date →
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.
Poincaré conjecture · publication v13
Record details
- Claim ID
- claim-poincare-three-topological
- Statement version
- 2
- SHA-256
- 623f5beb594a9e239386ff338920ea89201ea8e9f3db4c974f840101fbd2c437