Lean 4 formalizes Brouwer fixed point theorem, yields AI benchmark for proof understanding

Researchers Yuwei Lyu and Kai Li have achieved a significant milestone in formal mathematics by successfully encoding in Lean 4 a full combinatorial proof chain from Scarf's theorem to Brouwer's fixed point theorem, and ultimately to the existence of mixed Nash equilibria in finite games. Published on arXiv and accepted at the 3rd AI for Math Workshop (Toward Self-Evolving Scientific Agents), the 18-page paper details a rigorous formalization that traces Ivanov's indexed-order formulation of Scarf's theorem, uses a room-door incidence structure and parity argument, and instantiates the theorem on finite grids of the standard simplex. The work then extends to finite products of simplices via an explicit embedding-projection construction, enabling the proof of mixed Nash equilibrium existence through the Nash map.

As a secondary but equally impactful contribution, the authors introduce BrouwerBench — a preliminary 80-item benchmark built directly from the Lean formalization. Each item probes a specific aspect of proof structure, intended to evaluate AI models' understanding of formal mathematical reasoning. The benchmark is grounded entirely in the same Lean development, ensuring logical coherence and reproducibility. This dual deliverable — a verified theorem chain and a targeted benchmark for AI — positions the work both as a feat of formal verification and as a tool for advancing machine learning in mathematics.

For AI researchers and engineers, the implications are twofold: first, the Lean code provides a verified, executable route through some of the most fundamental results in game theory and topology; second, BrouwerBench offers a concrete, domain-specific test set for evaluating how well large language models grasp proof structures, beyond simple equation solving. As AI systems increasingly aim to assist in mathematical discovery, benchmarks like this become critical for measuring genuine reasoning capability. The paper also includes 11 tables that break down the formalization's structure, making it accessible to those new to Lean or to the theorem-proving pipeline.