Formalization of Brouwer's Fixed point Theorem

Stream: general

[Lyu Yuwei]

Just finished something exciting: I’ve finished the formalization of Scarf’s combinatorial theorem in Lean 4, and from it, I gave a constructive proof of Brouwer’s fixed point theorem :tada: The work is based on Nikolai V. Ivanov’s Beyond Sperner’s Lemma.

In this formalization, we discretize the simplex and apply Scarf’s combinatorial dominant-color framework with indexed linear orders to produce colorful points whose images have shrinking diameter, and the resulting convergent subsequence yields a limit z where coordinatewise monotonicity plus unit-sum constraints force f(z) = z.

I warmly invite you to have a look at my results and would greatly appreciate any comments or suggestions.

URL: https://github.com/math-xmum/Brouwer