feat: add Brouwer fixed-point theorem eval problem

LeanEval/Topology/Brouwer.lean

@@ -0,0 +1,39 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Topology
+
+/-!
+# Brouwer fixed-point theorem
+
+§33 of Oliver Knill's *Some Fundamental Theorems in Mathematics* (an
+additional statement in the section on game theory; Brouwer's theorem
+underlies Nash's 1950 proof of equilibrium existence). Every continuous
+self-map of a nonempty compact convex subset of `ℝᵈ` has a fixed point.
+
+mathlib has the Banach fixed-point theorem (`ContractingWith.exists_fixedPoint`)
+but it is strictly weaker — it requires a Lipschitz constant `< 1`.
+`grep -ri brouwer` in mathlib returns only Brouwerian lattices/logics, not
+the fixed-point theorem. It is theorem #36 on Freek Wiedijk's *Formalizing
+100 Theorems* list and is formalized in Lean **outside mathlib** (per
+mathlib's `docs/100.yaml` `links` entry), in Isabelle/AFP, HOL Light, and
+Coq.
+-/
+
+open Set
+
+/-- **Brouwer fixed-point theorem.** Every continuous self-map of a
+nonempty compact convex subset of `ℝᵈ` has a fixed point. -/
+@[eval_problem]
+theorem brouwer_fixed_point {d : ℕ}
+    {K : Set (EuclideanSpace ℝ (Fin d))}
+    (_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
+    (_hK_nonempty : K.Nonempty)
+    (f : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d))
+    (_hf_cont : ContinuousOn f K) (_hf_maps : MapsTo f K K) :
+    ∃ x ∈ K, f x = x := by
+  sorry
+
+end Topology
+end LeanEval

manifests/problems.toml

@@ -673,3 +673,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 = "brouwer_fixed_point"
+title = "Brouwer fixed-point theorem"
+test = false
+module = "LeanEval.Topology.Brouwer"
+holes = ["brouwer_fixed_point"]
+submitter = "Kim Morrison"
+notes = "§33 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (additional statement of the game-theory section; Brouwer underlies Nash's 1950 proof of equilibrium existence). Every continuous self-map of a nonempty compact convex K ⊆ ℝᵈ has a fixed point. Mathlib has the Banach fixed-point theorem (strictly weaker — needs Lipschitz < 1); `grep -ri brouwer` returns only Brouwerian lattices/logics. Brouwer is theorem #36 on Freek Wiedijk's 'Formalizing 100 Theorems' list and is formalized in Lean outside mathlib (per docs/100.yaml `links` entry), in Isabelle/AFP, HOL Light, and Coq."
+source = "L. E. J. Brouwer, Über Abbildung von Mannigfaltigkeiten, Math. Ann. 71 (1912). Listed as §33 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf); also #36 on Freek Wiedijk's 100 list (https://www.cs.ru.nl/~freek/100/)."
+informal_solution = "Reduce to the closed unit ball B^d via a homeomorphism (any nonempty compact convex K ⊆ ℝᵈ is homeomorphic to a closed ball of the appropriate dimension). On the ball, suppose for contradiction f has no fixed point; then for each x ∈ B^d the ray from f(x) through x meets ∂B^d in a unique point r(x), defining a continuous retraction r : B^d → ∂B^d with r|∂B^d = id. Such a retraction is impossible by a homotopy/homology argument (the sphere S^{d-1} is not contractible / has H_{d-1} = ℤ while the ball has trivial reduced homology), giving a contradiction. Alternative proofs go through Sperner's lemma, simplicial approximation, or homotopy invariance of degree."