Brouwer's fixed point theorem in Lean 4
There are several kinds of proofs for Brouwer's fixed point theorem. Nnevertheless, currently the theorem seems not part of Mathlib4.
Yet, we have seen some attempting its formal proof in Lean 4. For example, harfe/fixed-point-theorems-lean4 has done successfully by formalizing and relying on cubical Sperner's Lemma.
Today we asked Harmonics's Aristotle to prove the following variant of the theorem:
Every continuous function from a nonempty convex compact subset K of a Euclidean space to K itself has a fixed point.
Then the AI agent used the No-retraction theorem to get things done: shared link.