Proved
Established result in cited source ↗
Observed Oct 12, 2026
Theorem · version 1
The smooth three-dimensional theorem
Earlier version 1. View current version 2 →
Statement
Every closed, simply connected smooth three-manifold is diffeomorphic to the standard smooth three-sphere.
Assumptions
- Smoothness is additional structure; in dimension three the classification agrees with the topological theorem via smoothing and uniqueness of smooth structures.
Evidence
Source reports
Formal proofs
Smooth theorem · DifferentialGeometry release v0.1.3 ↗
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_holdsCommit 7a48598d35109aa99d1cc678e2724c213cdf4ff3
Smooth 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.smoothPoincareSkeletonCommit 1876d7dc2c85325a3f62ce9776af98f910c5db04
Smooth 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_sdiffeomorph_sphere_threeCommit 9454a4c25a2b923eb55dba3098f2d6ae0484d09b
Connections
In this problem · publication v5 · Selected context
Poincaré conjecture →
Equivalent formulation · Proved
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.
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 · Publication date Sep 28, 2026
Source-backed selection; publication and proof assessment are separate.
Revision & attribution
Source revision: 432c38f2aa5a30efb13871292d17b4a3309a496a. 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.
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
Established result in cited source ↗
Observed Oct 12, 2026 · Source passage →
Record details
- Claim ID
- claim-poincare-three-smooth
- Statement version
- 1
- SHA-256
- e45f19cb90efbe7f20adbf9a738378a811b039eef0cd3a7f8548f9c4ffd5d3da