Papers With

← All papers
First page of Formalizing Scarf, Brouwer, and Nash in Lean

Formalizing Scarf, Brouwer, and Nash in Lean

Yuwei Lyu, Kai Li

cs.LO Jul 7, 2026 · v1 cs.GT
formalization benchmark logic economics
Read PDF arXiv abstract Code
TL;DR
Formalizes in Lean 4 a combinatorial route from Scarf's theorem to Brouwer's fixed point theorem and mixed Nash equilibrium existence, using Mathlib.
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.
Problem

Brouwer's fixed point theorem and Nash equilibrium existence are usually invoked as black-box results, hiding the finite combinatorial structure that underlies them. A modular, inspectable formal proof route exposing this structure was lacking in Lean.

Approach

The development follows Ivanov's indexed-order formulation of Scarf's combinatorial theorem, formalizing dominant sets, cells, rooms, doors, and the parity argument yielding a colorful room. The theorem is instantiated on finite grids of the standard simplex, and compactness, continuity, and vanishing-diameter estimates yield a Brouwer fixed point. An explicit embedding–projection construction extends this to finite products of simplices, which is applied to the Nash map to prove mixed equilibrium existence. Intermediate proof objects are exposed as named Lean definitions and lemmas.

Results

A complete Lean 4 formalization spanning Scarf, Brouwer (standard simplex and products), and Nash equilibrium existence is provided. As a by-product, BrouwerBench, an 80-item Lean-grounded pilot benchmark probing proof-structure understanding, is derived from the development.