Source · Paper

A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture

Ziyang Qin · Yuan Liao · Ayush Khaitan · Bennett Chow

PreprintPublication date Sep 27, 2026

Open paper ↗

Reading source record arxiv-2609.33842v1. View default cited record →

Overview

A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture

Source-backed selection; publication and proof assessment are separate.

1 cited passage ↓1 problem ↓Record arxiv-2609.33842v1 ↓

Passages

The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.

Passage 1 · OpenMath paraphrasePermalink

§1, Theorems 1–3; §3, release and verification

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.

Read at source ↗13 recorded uses ↓

Passage details

Passage ID: poincare-conjecture:entry:qin-formal:v1

Source item: §1, Theorems 1–3; §3, release and verification

Source record: qin-liao-khaitan-chow-poincare@arxiv-2609.33842v1

Used in

Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.

Poincaré conjecture →

Problem publication v13

Smoothing a topological three-manifold →

Source assessment

Proved

Established result in cited source

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

Observed Oct 12, 2026

Assessment source ↗Statement v1 →

§1, Theorems 1–3; §3, release and verification ↑

Statement

Statement v1 →

§1, Theorems 1–3; §3, release and verification ↑

The topological three-dimensional Poincaré theorem →

Formal declaration

Topological theorem · DifferentialGeometry release v0.1.3

Statement v2 →Inspect formal evidence ↓

§1, Theorems 1–3; §3, release and verification ↑

Scope

The topological three-dimensional Poincaré theorem

Statement v2 →

§1, Theorems 1–3; §3, release and verification ↑

Statement

Statement v2 →

§1, Theorems 1–3; §3, release and verification ↑

The smooth three-dimensional theorem →

Formal declaration

Smooth theorem · DifferentialGeometry release v0.1.3

Statement v2 →Inspect formal evidence ↓

§1, Theorems 1–3; §3, release and verification ↑

Scope

The smooth three-dimensional theorem

Statement v2 →

§1, Theorems 1–3; §3, release and verification ↑

Statement

Statement v2 →

§1, Theorems 1–3; §3, release and verification ↑

Finite extinction in the simply connected case →

Statement

Statement v1 →

§1, Theorems 1–3; §3, release and verification ↑

Problem context · 4 citations

Research activity

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.

View in problem →

§1, Theorems 1–3; §3, release and verification ↑

History

A source-pinned Lean formalization report

View in problem →

§1, Theorems 1–3; §3, release and verification ↑

Question

Poincaré conjecture

View in problem →

§1, Theorems 1–3; §3, release and verification ↑

Files

Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.

Formal declarations

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_conjecture

Commit 7a48598d35109aa99d1cc678e2724c213cdf4ff3

A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture: §1, Theorems 1–3; §3, release and verification →

The topological three-dimensional Poincaré theorem · statement v2 →

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_holds

Commit 7a48598d35109aa99d1cc678e2724c213cdf4ff3

A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture: §1, Theorems 1–3; §3, release and verification →

The smooth three-dimensional theorem · statement v2 →

Credits

Recorded authorship

Ziyang Qin · Yuan Liao · Ayush Khaitan · Bennett Chow

Ziyang Qin; Yuan Liao; Ayush Khaitan; Bennett Chow

AI involvement reported by the source

Authors report automated assistance; OpenMath has not independently assessed that workflow.

Versions

OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.

arxiv-2609.33842v1 · selectedObserved Oct 12, 2026 · used in current publications
A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture

Record details

Source ID: qin-liao-khaitan-chow-poincare
Record ID: qin-liao-khaitan-chow-poincare@arxiv-2609.33842v1
Recorded title: A Lean Formalization of the Hamilton–Perelman Proof of the Three-Dimensional Poincaré Conjecture
Revision: arxiv-2609.33842v1
Observed: Oct 12, 2026
Source updated: Not recorded
Content SHA-256: Not recorded
Update method: Manual source review; publish new observations with immutable versions
Identifier policy: Source revision plus exact passage or declaration; no fuzzy identity merge
Check interval: 90 days
Rights: metadata-link
License: Metadata, links and original OpenMath paraphrases only

Follow the original source for authoritative statements and reuse terms.

Source terms ↗