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

LeanEval/Topology/Poincare3DSmooth.lean

@@ -0,0 +1,42 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Topology
+
+/-!
+# 3D smooth Poincaré conjecture (Perelman)
+
+A `proof_wanted` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Every
+simply connected compact Hausdorff 3-manifold that admits a smooth structure
+is **diffeomorphic** to the standard 3-sphere `𝕊³`.
+
+This is the smooth-category strengthening of the topological 3D Poincaré
+conjecture, also proved by Perelman in 2002–2003. In dimension 3 the smooth
+and topological Poincaré conjectures are equivalent (every topological
+3-manifold admits a unique smooth structure, by Moise's theorem), but the
+formal Lean statement carries the smooth structure explicitly via
+`IsManifold (𝓡 3) ∞ M` and concludes with a diffeomorphism in the manifold
+type `M ≃ₘ⟮𝓡 3, 𝓡 3⟯ 𝕊³`.
+
+mathlib has `ChartedSpace`, `IsManifold`, `Diffeomorph`, `SimplyConnectedSpace`,
+`CompactSpace`, and the unit sphere as a smooth manifold but no Ricci flow,
+no Hamilton–Perelman surgery, and no Moise theorem.
+-/
+
+open scoped Manifold ContDiff
+open Metric (sphere)
+
+/-- **3D smooth Poincaré conjecture** (Perelman, 2002–2003). Every simply
+connected compact Hausdorff smooth 3-manifold is diffeomorphic to the
+standard 3-sphere `𝕊³`. -/
+@[eval_problem]
+theorem poincare_3d_smooth
+    {M : Type*} [TopologicalSpace M] [T2Space M]
+    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] [IsManifold (𝓡 3) ∞ M]
+    [SimplyConnectedSpace M] [CompactSpace M] :
+    Nonempty (M ≃ₘ⟮𝓡 3, 𝓡 3⟯ sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) := by
+  sorry
+
+end Topology
+end LeanEval

manifests/problems/poincare_3d_smooth.toml

@@ -0,0 +1,9 @@
+id = "poincare_3d_smooth"
+title = "3D smooth Poincaré conjecture (Perelman)"
+test = false
+module = "LeanEval.Topology.Poincare3DSmooth"
+holes = ["poincare_3d_smooth"]
+submitter = "Kim Morrison"
+notes = "Every simply connected compact Hausdorff smooth 3-manifold is diffeomorphic to 𝕊³. Recorded as `proof_wanted SimplyConnectedSpace.nonempty_diffeomorph_sphere_three` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. The smooth-category strengthening of the topological 3D Poincaré conjecture; also Perelman 2002-2003. In dim 3 the smooth and topological versions are equivalent (Moise's theorem says every topological 3-manifold admits a unique smooth structure), but the Lean statement carries the smooth structure explicitly. Mathlib has all the differential-topology / manifold scaffolding but neither Ricci flow nor Moise's theorem."
+source = "G. Perelman, three arXiv preprints 2002-2003 (math/0211159, math/0303109, math/0307245). Recorded as a `proof_wanted` in Mathlib/Geometry/Manifold/PoincareConjecture.lean. In dim 3, Smooth ⇔ PL ⇔ Topological via Moise (1952) / Bing (1959)."
+informal_solution = "Apply the topological 3D Poincaré conjecture to obtain a homeomorphism M ≃ₜ S³, then promote it to a diffeomorphism via Moise's theorem (every topological 3-manifold admits a unique smooth structure up to diffeomorphism), or equivalently observe that Hamilton-Perelman Ricci flow with surgery runs in the smooth category and produces a smooth diffeomorphism directly. Either route involves the same Perelman input on the geometric side; the dim-3 special feature is Moise/Bing which collapses the smooth/topological distinction (false in dim 4 and above)."