feat: add 4D topological Poincaré conjecture (Freedman) eval problem

LeanEval/Topology/Poincare4DTopological.lean

@@ -0,0 +1,43 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Topology
+
+/-!
+# 4D topological Poincaré conjecture (Freedman)
+
+A specialization of mathlib's generalized `proof_wanted
+ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in
+`Mathlib/Geometry/Manifold/PoincareConjecture.lean`, restricted to
+dimension 4: every Hausdorff 4-manifold homotopy-equivalent to the standard
+4-sphere `𝕊⁴` is homeomorphic to `𝕊⁴`.
+
+This is Michael Freedman's 1982 theorem (Freedman, *The topology of
+four-dimensional manifolds*, J. Differential Geom. 17), for which he was
+awarded the Fields Medal in 1986. The proof uses Casson handles and the
+"Bing topology" infinite-process construction; the corresponding **smooth**
+4D Poincaré conjecture (every smooth homotopy 4-sphere is diffeomorphic
+to `𝕊⁴`) remains famously **open** and is not included as an eval problem.
+
+mathlib has homotopy equivalences (`≃ₕ`), homeomorphisms (`≃ₜ`),
+`ChartedSpace`, and the unit sphere as a topological space — but no Casson
+handles, no Freedman's theorem, and no 4D Poincaré conjecture.
+-/
+
+open Metric (sphere)
+open ContinuousMap
+
+/-- **4D topological Poincaré conjecture** (Freedman, 1982). Every Hausdorff
+4-manifold that is homotopy-equivalent to the standard 4-sphere `𝕊⁴` is
+homeomorphic to `𝕊⁴`. -/
+@[eval_problem]
+theorem poincare_4d_topological
+    {M : Type*} [TopologicalSpace M] [T2Space M]
+    [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M]
+    (_h : M ≃ₕ sphere (0 : EuclideanSpace ℝ (Fin 5)) 1) :
+    Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 5)) 1) := by
+  sorry
+
+end Topology
+end LeanEval

manifests/problems/poincare_4d_topological.toml

@@ -0,0 +1,9 @@
+id = "poincare_4d_topological"
+title = "4D topological Poincaré conjecture (Freedman)"
+test = false
+module = "LeanEval.Topology.Poincare4DTopological"
+holes = ["poincare_4d_topological"]
+submitter = "Kim Morrison"
+notes = "Every Hausdorff 4-manifold homotopy-equivalent to 𝕊⁴ is homeomorphic to 𝕊⁴. Specialization to n = 4 of mathlib's generalized `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Michael Freedman's 1982 theorem (J. Differential Geom. 17), Fields Medal 1986. Proof uses Casson handles and the Bing-topology infinite-process construction. The corresponding smooth 4D Poincaré conjecture (every smooth homotopy 4-sphere is diffeomorphic to S⁴) remains famously OPEN and is not included here. Mathlib has the homotopy-equiv / homeo / ChartedSpace scaffolding but no Casson handles or Freedman's theorem."
+source = "M. H. Freedman, The topology of four-dimensional manifolds, J. Differential Geom. 17 (1982), 357-453. Specialization of `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in Mathlib/Geometry/Manifold/PoincareConjecture.lean."
+informal_solution = "Freedman's main theorem: every topological 4-manifold homotopy equivalent to a topological model is homeomorphic to it, provided one can construct topological Casson handles. The construction of Casson handles is via a Bing-style limiting process (countably many handle additions, infinite tower of 2-handles) that produces a topological — but not smooth — 4-ball. Applying this to a homotopy 4-sphere M, one writes M as the union of two 2-handlebodies along their boundary, replaces handles with Casson handles, and assembles a homeomorphism to S⁴. The smooth analogue is open because Casson handles need not be smoothly standard (Donaldson's invariants distinguish smooth structures in dim 4)."