{"ID":6023447,"CreatedAt":"2026-07-08T01:00:23.257252134Z","UpdatedAt":"2026-07-10T08:15:11.905439937Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.05987","arxiv_id":"2607.05987","title":"Formalizing Scarf, Brouwer, and Nash in Lean","abstract":"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 development follows Ivanov's indexed-order formulation of Scarf's theorem, formalizes the room--door incidence structure and parity argument, instantiates the theorem on finite grids of the standard simplex, and carries out the compactness and continuity argument needed to obtain a fixed point. We then extend the result to finite products of simplices by an explicit embedding--projection construction and use this product theorem to prove mixed Nash equilibrium existence via the Nash map. As a secondary by-product, we derive BrouwerBench, a preliminary 80-item Lean-grounded benchmark for probing proof-structure understanding within this single formal development.","short_abstract":"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 development follows Ivanov's indexed-order formulation of Scarf's theorem, formalizes the room--door incidence structure and parity argument, ins...","url_abs":"https://arxiv.org/abs/2607.05987","url_pdf":"https://arxiv.org/pdf/2607.05987v1","authors":"[\"Yuwei Lyu\",\"Kai Li\"]","published":"2026-07-07T08:18:43Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.GT\"]","methods":"[]","has_code":false}