Brouwer fixed-point theorem

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.

theorem declaration uses `sorry`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 := byd:ℕK:Set (EuclideanSpace ℝ (Fin d))_hK_compact:IsCompact K_hK_convex:Convex ℝ K_hK_nonempty:K.Nonemptyf:EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)_hf_cont:ContinuousOn f K_hf_maps:MapsTo f K K⊢ ∃ x ∈ K, f x = x
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on May 25, 2026

• @rishistyping with Stealth Model on May 26, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 28, 2026

• @JohnEdwardJennings with Aristotle (Harmonic) on May 31, 2026