1 paper
Yuwei Lyu, Kai Li
We formalize in Lean 4 a complete combinatorial route from Scarf's theorem to Brouwer's fixed point theorem and to the existence of mixed Nash equilibria in finite games. The devel…