From c6141debe8f08144887047ce2c14fca41d052989 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 23 May 2026 13:00:25 +0000
Subject: [PATCH] =?UTF-8?q?feat:=20add=203D=20topological=20Poincar=C3=A9?=
 =?UTF-8?q?=20conjecture=20(Perelman)=20eval=20problem?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds the 3D topological Poincaré conjecture as a new eval
problem: every simply connected compact Hausdorff 3-manifold is
homeomorphic to 𝕊³. Recorded in mathlib as `proof_wanted
SimplyConnectedSpace.nonempty_homeomorph_sphere_three` in
`Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Proved by
Perelman 2002-2003 via Hamilton's Ricci flow with surgery; one of the
seven Millennium Problems.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 LeanEval/Topology/Poincare3DTopological.lean | 38 ++++++++++++++++++++
 manifests/problems.toml                      | 11 ++++++
 2 files changed, 49 insertions(+)
 create mode 100644 LeanEval/Topology/Poincare3DTopological.lean

diff --git a/LeanEval/Topology/Poincare3DTopological.lean b/LeanEval/Topology/Poincare3DTopological.lean
new file mode 100644
index 0000000..331ca01
--- /dev/null
+++ b/LeanEval/Topology/Poincare3DTopological.lean
@@ -0,0 +1,38 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Topology
+
+/-!
+# 3D topological Poincaré conjecture (Perelman)
+
+A `proof_wanted` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Every
+simply connected compact Hausdorff 3-manifold is homeomorphic to the standard
+3-sphere `𝕊³`.
+
+Proved by Grigori Perelman in 2002–2003 via Hamilton's Ricci flow with surgery
+(Perelman's three preprints on the arXiv; Fields Medal awarded but declined,
+2006; Clay Millennium Prize awarded 2010, also declined). One of the seven
+original Millennium Problems.
+
+mathlib has `ChartedSpace`, `SimplyConnectedSpace`, `CompactSpace`, `T2Space`,
+`Homeomorph` (`≃ₜ`), and the unit sphere as a smooth manifold but no
+Ricci flow, no Hamilton–Perelman surgery, and no Poincaré conjecture itself.
+-/
+
+open Metric (sphere)
+
+/-- **3D topological Poincaré conjecture** (Perelman, 2002–2003). Every
+simply connected compact Hausdorff 3-manifold is homeomorphic to the
+standard 3-sphere `𝕊³`. -/
+@[eval_problem]
+theorem poincare_3d_topological
+    {M : Type*} [TopologicalSpace M] [T2Space M]
+    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M]
+    [SimplyConnectedSpace M] [CompactSpace M] :
+    Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) := by
+  sorry
+
+end Topology
+end LeanEval
diff --git a/manifests/problems.toml b/manifests/problems.toml
index 87a63eb..b368423 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -682,3 +682,14 @@ module = "LeanEval.Geometry.Uniformization"
 holes = ["uniformization"]
 submitter = "Junyan Xu"
 source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1."
+
+[[problem]]
+id = "poincare_3d_topological"
+title = "3D topological Poincaré conjecture (Perelman)"
+test = false
+module = "LeanEval.Topology.Poincare3DTopological"
+holes = ["poincare_3d_topological"]
+submitter = "Kim Morrison"
+notes = "Every simply connected compact Hausdorff 3-manifold is homeomorphic to 𝕊³. Recorded as `proof_wanted SimplyConnectedSpace.nonempty_homeomorph_sphere_three` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Proved by Perelman in 2002-2003 via Hamilton's Ricci flow with surgery; one of the seven Millennium Problems. Mathlib has ChartedSpace, SimplyConnectedSpace, CompactSpace, T2Space, Homeomorph and the unit sphere as a smooth manifold but no Ricci flow, no Hamilton-Perelman surgery, and no Poincaré conjecture itself."
+source = "G. Perelman, The entropy formula for the Ricci flow and its geometric applications (arXiv:math/0211159, 2002); Ricci flow with surgery on three-manifolds (arXiv:math/0303109, 2003); Finite extinction time for the solutions to the Ricci flow on certain three-manifolds (arXiv:math/0307245, 2003). Recorded as a `proof_wanted` in Mathlib/Geometry/Manifold/PoincareConjecture.lean. Originally conjectured by Henri Poincaré in 1904."
+informal_solution = "Run Ricci flow ∂g/∂t = -2 Ric(g) on M with surgery to remove finite-time singularities (Hamilton's program, completed by Perelman). The flow simplifies the metric, and Perelman's monotonicity formulas (reduced volume, ℒ-functional, no local collapsing) together with the canonical-neighbourhood theorem control the geometry. In finite time the flow either becomes extinct (M is a connected sum of spherical space forms and S²×S¹s, in particular when π_1(M) = 1, M = S³) or decomposes M along incompressible 2-tori into pieces of one of Thurston's eight geometric types; the simply-connected hypothesis rules out the toroidal decomposition and the spherical-space-form ambiguity, leaving M ≃ S³."