Open
Open question in cited source ↗
From Knots to Four-Manifolds · §3, Conjecture 3.1 and preceding topological classification →
Observed Oct 12, 2026
Conjecture · version 1
The smooth four-dimensional Poincaré question
Statement
Every closed smooth four-manifold homotopy equivalent to the four-sphere is diffeomorphic to the standard smooth four-sphere.
Assumptions
- This is a separate conjecture in dimension four; simple connectivity alone is insufficient for its hypothesis.
- Dimension
- 4
- Category
- Smooth · diffeomorphism
Evidence
Source reports
Connections
In this problem · publication v11 · Selected context
Poincaré conjecture →
Different statement · related variant · Open
Related statements
Homeomorphism and diffeomorphism are different requirements in dimension four.
The proved topological theorem does not settle the smooth conjecture.
Details & sources
The topological four-dimensional theorem →
Proved · version 1
Every closed topological four-manifold homotopy equivalent to the four-sphere is homeomorphic to the four-sphere.
- Freedman’s topological conclusion does not identify a smooth structure or imply the smooth four-dimensional conjecture.
Scope: Freedman’s topological conclusion does not identify a smooth structure or imply the smooth four-dimensional conjecture.
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 →Analogue
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.
In this problem · publication v13
Poincaré conjecture →
Different statement · related variant · Open
Related statements
Homeomorphism and diffeomorphism are different requirements in dimension four.
The proved topological theorem does not settle the smooth conjecture.
Details & sources
The topological four-dimensional theorem →
Proved · version 1
Every closed topological four-manifold homotopy equivalent to the four-sphere is homeomorphic to the four-sphere.
- Freedman’s topological conclusion does not identify a smooth structure or imply the smooth four-dimensional conjecture.
Scope: Freedman’s topological conclusion does not identify a smooth structure or imply the smooth four-dimensional conjecture.
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 →Analogue
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
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.
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
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.
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.
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.
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.
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.
Open
Open question in cited source ↗
Observed Oct 12, 2026 · Source passage →
Record details
- Claim ID
- claim-poincare-smooth-four
- Statement version
- 1
- SHA-256
- a720bdcc5b4d20114d6def3bf2dec78b3365e16d5b355b21b05fc9637321c536