feat: add 3D topological Poincaré conjecture (Perelman) eval problem

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

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³."