Clay · Millennium Problems ↗
Solved · observed Oct 1, 2026
Source status date unavailable · observed Oct 1, 2026
The cited source item and version only; this is not an independent OpenMath assessment.
Publication v8
Record details
Poincaré conjecture →Coverage & review
Coverage of this curation
The accepted topological theorem, smooth formulation, proof ingredients, dimension-four scope and recent formalization evidence.
Formal proofs: 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.
AI-assisted work: Both formalization projects self-report automated assistance; this attribution is separate from theorem truth and verification evidence.
Search scope & review
Clay’s official description and Morgan–Tian account; Perelman’s finite-extinction paper; Manolescu’s 2026 survey; two 2026 formalization papers, exact public source revisions and the FrenzyMath verification report; Mathlib wanted declarations.
Checked Oct 12, 2026 · independent review pending.
- Selected sources and milestones; this is not an exhaustive literature review.
- Independent mathematical review and OpenMath reproduction of external proof checks remain pending.
General status observations
Source identities & rights
Clay · Millennium Problems ↗
Clay Mathematics Institute · metadata-link · Not established; links and OpenMath paraphrases only
Store metadata and original OpenMath paraphrases; follow the original source for authoritative wording. Rights / source terms
1 cited entry · exact source identity
- Version
- clay-millennium@observed-2026-10-01
- Revision
- observed-2026-10-01
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-01
- Check cadence
- 30 days
- https://www.claymath.org/millennium/poincare-conjecture/ ↗
poincare-conjecture:entry:0:v1
Ricci Flow and the Poincaré Conjecture ↗
John Morgan; Gang Tian · metadata-link · Metadata, links and original OpenMath paraphrases only
Follow the original source for authoritative statements and reuse terms. Rights / source terms
1 cited entry · exact source identity
- Version
- morgan-tian-poincare@clay-monograph-3-2007
- Revision
- clay-monograph-3-2007
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-12
- Check cadence
- 90 days
- Clay monograph 3; introduction, Theorem 0.1 and Corollary 0.2 ↗
poincare-conjecture:entry:proof:v1
Finite extinction time for the solutions to the Ricci flow on certain three-manifolds ↗
Grigori Perelman · metadata-link · Metadata, links and original OpenMath paraphrases only
Follow the original source for authoritative statements and reuse terms. Rights / source terms
1 cited entry · exact source identity
- Version
- perelman-extinction@arxiv-math-0307245v1
- Revision
- arxiv-math-0307245v1
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-12
- Check cadence
- 90 days
- Abstract; finite-extinction argument ↗
poincare-conjecture:entry:extinction:v1
The Poincaré Conjecture · official description ↗
John Milnor · metadata-link · Metadata, links and original OpenMath paraphrases only
Follow the original source for authoritative statements and reuse terms. Rights / source terms
1 cited entry · exact source identity
- Version
- milnor-poincare-description@clay-description-observed-2026-10-12
- Revision
- clay-description-observed-2026-10-12
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-12
- Check cadence
- 90 days
- §§1–3; dimension-three comparison on page 5 ↗
poincare-conjecture:entry:dimension-scope:v1
From Knots to Four-Manifolds ↗
Ciprian Manolescu · metadata-link · Metadata, links and original OpenMath paraphrases only
Follow the original source for authoritative statements and reuse terms. Rights / source terms
1 cited entry · exact source identity
- Version
- manolescu-four-manifolds@icm-2026-doi-25M1806703
- Revision
- icm-2026-doi-25M1806703
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-12
- Check cadence
- 90 days
- §3, Conjecture 3.1 and preceding topological classification ↗
poincare-conjecture:entry:smooth-four:v1
A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture ↗
Ziyang Qin; Yuan Liao; Ayush Khaitan; Bennett Chow · metadata-link · Metadata, links and original OpenMath paraphrases only
Follow the original source for authoritative statements and reuse terms. Rights / source terms
1 cited entry · exact source identity
- Version
- qin-liao-khaitan-chow-poincare@arxiv-2609.33842v1
- Revision
- arxiv-2609.33842v1
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-12
- Check cadence
- 90 days
- §1, Theorems 1–3; §3, release and verification ↗
poincare-conjecture:entry:qin-formal:v1
An AI-Assisted Formalization of the Poincaré Conjecture ↗
Zhiyuan Zhang; Axel Delaval; Leheng Chen; Jinxuan Chen; Jie Xu; Yuxuan Liao; Jiedong Jiang; Chunlei Liu; Bin Dong · metadata-link · Metadata, links and original OpenMath paraphrases only
Follow the original source for authoritative statements and reuse terms. Rights / source terms
1 cited entry · exact source identity
- Version
- frenzymath-poincare@arxiv-2610.08329v1
- Revision
- arxiv-2610.08329v1
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-12
- Check cadence
- 90 days
- Formal theorem endpoints and verification discussion ↗
poincare-conjecture:entry:frenzy-formal:v1
Poincaré comparator integration verification ↗
FrenzyMath contributors · metadata-link · Metadata, links and original OpenMath paraphrases only
Follow the original source for authoritative statements and reuse terms. Rights / source terms
1 cited entry · exact source identity
- Version
- frenzymath-poincare-verification@432c38f2aa5a30efb13871292d17b4a3309a496a-metadata-v2
- Revision
- 432c38f2aa5a30efb13871292d17b4a3309a496a; bibliographic metadata corrected 2026-10-12
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-12
- Check cadence
- 90 days
- Local integration verification; verification.json beside README ↗
poincare-conjecture:entry:frenzy-verification:v2
Mathlib · wanted Poincaré statements ↗
Mathlib contributors · metadata-link · Metadata, links and original OpenMath paraphrases only
Follow the original source for authoritative statements and reuse terms. Rights / source terms
1 cited entry · exact source identity
- Version
- mathlib-poincare-wanted@9454a4c25a2b923eb55dba3098f2d6ae0484d09b
- Revision
- 9454a4c25a2b923eb55dba3098f2d6ae0484d09b
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-12
- Check cadence
- 90 days
- SimplyConnectedSpace.nonempty_homeomorph_sphere_three and nonempty_sdiffeomorph_sphere_three ↗
poincare-conjecture:entry:wanted-statements:v1
Poincaré comparator integration verification ↗
FrenzyMath contributors · metadata-link · Metadata, links and original OpenMath paraphrases only
Follow the original source for authoritative statements and reuse terms. Rights / source terms
1 cited entry · exact source identity
- Version
- frenzymath-poincare-verification@432c38f2aa5a30efb13871292d17b4a3309a496a
- Revision
- 432c38f2aa5a30efb13871292d17b4a3309a496a
- Content SHA-256
- No upstream byte snapshot retained; linked metadata only
- Source update
- Unavailable
- Observed
- 2026-10-12
- Check cadence
- 90 days
- Local integration verification; verification.json beside README ↗
poincare-conjecture:entry:frenzy-verification:v1
Publication history
- Problem ID
- problem-poincare-conjecture
- Publication checksum
- 5a1345f0f83e2038524fecd3d1e63e3c68012df7551779706460a2bb94c93c92
- Published
- 2026-10-12T11:38:08.452040+00:00
- Publication reason
- Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 1 · Sep 30, 2026
Initial checked pilot publication; source attribution, rights, wording and coverage reviewed by OpenMath staff.
- Version 2 · Sep 30, 2026
Correct classification to MSC2020 57K30 and 57R60 after checking the official AMS/zbMATH taxonomy; retain the attributed Clay status.
- Version 3 · Oct 10, 2026
Add cited resolution scope and consolidate equivalent prime formulations and supporting Claims; mathematical evidence and execution review remain distinct.
- Version 4 · Oct 11, 2026
Publish checked pilot curation with canonical Claims and scoped progress; preserve exact source revisions, assumptions, coverage limits and historical publications. External artifacts and OpenMath execution remain distinct.
- Version 5 · Oct 12, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 6 · Oct 12, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 7 · Oct 12, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 8 · Oct 12, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 9 · Oct 13, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 10 · Oct 14, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 11 · Oct 15, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 12 · Oct 20, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 13 · Oct 20, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.