REVIEW 2 major objections 10 references
Formalizing Scarf, Brouwer, and Nash in Lean
T0 review · 2 major / 0 minor · reviewed 2026-07-08 · grok-4.5
Pith's one-line read A complete Lean 4 formalization traces Scarf’s combinatorial theorem through Brouwer fixed points to mixed Nash equilibria in finite games.
desk verdict End-to-end Lean 4 Scarf→Brouwer→Nash along Ivanov’s combinatorial route is a real formalization artifact if the code builds; continuum lift and product embedding are the only places the completeness claim can quietly fail. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The room–door incidence structure and parity argument of Ivanov’s indexed-order Scarf theorem, instantiated on finite grids of the simplex and lifted by a compactness–continuity argument; the chain is then extended by an explicit embedding–projection construction that supplies the product-of-simplices domain required by the Nash map.
What would settle it
A failed Lean type-check of the final Nash-existence theorem, or an explicit counter-example showing that the compactness–continuity lift (or the embedding–projection step) fails to produce a genuine fixed point of a continuous map on the continuum simplex or on a finite product of simplices.
Extended reading notes
Core claim
The authors give a complete Lean 4 formalization of a combinatorial route that begins with Scarf’s theorem in Ivanov’s indexed-order form, produces almost-fixed points on finite grids of the standard simplex, lifts them by compactness and continuity to a Brouwer fixed point, extends the result to finite products of simplices by an explicit embedding–projection construction, and obtains mixed Nash equilibria for finite games via the Nash map. The same development yields BrouwerBench, a preliminary 80-item Lean-grounded benchmark for proof-structure understanding.
Load-bearing premise
The discrete almost-fixed points found on finite grids of the simplex, together with the compactness and continuity arguments written in Lean, really do close the continuum limit to a true Brouwer fixed point without hidden gaps, and the embedding–projection construction correctly transfers the product case needed for the Nash map.
Editorial extensions
If this is right
- Machine-checked existence of mixed Nash equilibria for any finite normal-form game is available as an importable Lean theorem.
- Brouwer’s fixed-point theorem on the standard simplex and on finite products of simplices is available as a formal Lean statement proved from combinatorial premises.
- Later developments that need a combinatorial fixed-point engine can reuse the Scarf-grid and lift lemmas directly.
- BrouwerBench supplies a single-development suite of 80 Lean items for testing whether a prover recovers the intended proof structure of this chain.
Reading between the lines
- The same embedding–projection pattern could be reused to formalize other multi-player fixed-point arguments that live on products of strategy simplices.
- If the compactness–continuity lift were made fully constructive with effective moduli, the development could yield computable approximate equilibria rather than bare existence.
- Because BrouwerBench’s items come from one tightly coupled development, they form a natural stress test for whether retrieval-augmented provers keep global obligations coherent across a long dependency chain.
- The formal Scarf route may serve as a template for mechanizing other classical combinatorial existence proofs that remain only sketchily formalized.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper presents a Lean 4 formalization of a combinatorial route from Scarf's theorem (Ivanov's indexed-order formulation, room–door incidence and parity) through finite grids of the standard simplex and a compactness–continuity lift to Brouwer's fixed-point theorem, then via an explicit embedding–projection product construction and the Nash map to mixed Nash equilibrium existence for finite games, with BrouwerBench as an 80-item by-product.
Significance. If the Lean development compiles end-to-end as claimed, this would be a substantial contribution to formalized mathematics: a machine-checked combinatorial path Scarf→Brouwer→Nash, with explicit continuum lift and product extension, plus a reusable Lean-grounded benchmark. Machine-checked proofs and a parameter-free classical route are clear strengths.
major comments (2)
- The continuum lift from Scarf grid almost-fixed-points to exact Brouwer (compactness of Δ and continuity of f) is load-bearing and not fully verifiable from the abstract alone; the manuscript must show that the final Brouwer statement is the classical continuous-map theorem with no residual discreteness hypotheses (Mathlib topology, sequential/filter compactness).
- The explicit embedding–projection e:∏Δ^{n_i}↪Δ^N, p:Δ^N→∏Δ^{n_i} must correctly conjugate fixed points of the lifted map back to fixed points of the Nash map on the product; a mismatch would break Nash existence even if single-simplex Brouwer is correct.
Simulated Author's Rebuttal
We thank the referee for a careful reading and for isolating the two load-bearing steps on which the Scarf→Brouwer→Nash chain depends: the continuum lift to classical Brouwer, and the fixed-point transfer through the product embedding–projection. Both points concern presentation and verifiability of statements already present in the Lean development rather than gaps in the combinatorial core. We address each by making the final classical statements, the Mathlib topology used, and the conjugation lemmas fully explicit in the revised manuscript. We believe these revisions resolve the concerns that motivated the major-revision recommendation.
read point-by-point responses
-
Referee: The continuum lift from Scarf grid almost-fixed-points to exact Brouwer (compactness of Δ and continuity of f) is load-bearing and not fully verifiable from the abstract alone; the manuscript must show that the final Brouwer statement is the classical continuous-map theorem with no residual discreteness hypotheses (Mathlib topology, sequential/filter compactness).
Authors: We agree that the continuum lift is load-bearing and that the manuscript must make the classical character of the final statement unmistakable. In the development the terminal theorem is the standard Brouwer fixed-point theorem: every continuous self-map of the standard simplex has a fixed point. Continuity is Mathlib Continuous on the simplex as a closed subset of Euclidean space; compactness is Mathlib IsCompact (via sequential compactness / filter compactness of the compact metric space Δ). The argument is: for each mesh, Ivanov–Scarf on the grid yields an almost-fixed grid point; a convergent subsequence is extracted by compactness; continuity of f passes the almost-fixed property to the limit, producing an exact fixed point. No residual discreteness, mesh, or combinatorial hypotheses remain in the final statement. We will revise the relevant section to display the exact Lean statement of Brouwer, name the Mathlib compactness and continuity lemmas used, and spell out the three-step lift so that classicality is verifiable from the text alone. revision: yes
-
Referee: The explicit embedding–projection e:∏Δ^{n_i}↪Δ^N, p:Δ^N→∏Δ^{n_i} must correctly conjugate fixed points of the lifted map back to fixed points of the Nash map on the product; a mismatch would break Nash existence even if single-simplex Brouwer is correct.
Authors: We agree that correct conjugation is essential: a mismatch would invalidate the Nash existence theorem even with single-simplex Brouwer in hand. The construction supplies an embedding e : ∏_i Δ^{n_i} ↪ Δ^N and a projection p : Δ^N → ∏_i Δ^{n_i} with p ∘ e = id on the product. The product (Nash) map g on ∏ Δ^{n_i} is lifted to a continuous self-map F of Δ^N by F = e ∘ g ∘ p (up to the standard affine identification of the product with its image). We prove the conjugation lemma: if F(y) = y then p(y) is a fixed point of g. Thus every fixed point of the lifted map on the large simplex projects to a fixed point of the Nash map on the product, and mixed Nash existence follows. This transfer is machine-checked. We will revise the product section to state the conjugation lemma explicitly, record p ∘ e = id and the definition of F, and add a short commutative diagram so that fixed-point transfer is transparent in the text. revision: yes
Circularity Check
No significant circularity: Lean 4 formalization of classical Scarf–Brouwer–Nash combinatorial route
full rationale
The paper is a machine-checked Lean 4 formalization of external classical theorems (Scarf via Ivanov’s indexed-order room–door parity, Brouwer via grid almost-fixed-points plus compactness/continuity, and mixed Nash via the Nash map on a product of simplices obtained by an explicit embedding–projection). Target statements are textbook results, not quantities fitted from data or defined in terms of the claimed outputs. There is no free-parameter fit renamed as a prediction, no self-definitional loop (X defined via Y then used to derive Y), no uniqueness theorem imported from the authors’ prior work as a load-bearing external fact, and no ansatz smuggled in via self-citation. Any reliance on Mathlib topology or on the authors’ own Lean development is independent once machine-checked and does not force the classical statements by construction. The continuum lift and product embedding are potential correctness gaps, not circularity. Residual circularity is zero; score 0 with empty steps is the warranted finding.
Assumptions & free parameters
assumptions (4)
- domain assumption Scarf/Ivanov combinatorial hypotheses: admissible labeling (indexed-order formulation) on a triangulation or grid of the simplex yields a fully labeled small simplex via room–door incidence and a parity argument.
- standard math Standard topology of the simplex: compactness of the standard simplex (and finite products) and continuity of the maps under consideration suffice to pass from discrete almost-fixed-points to a continuum fixed point.
- domain assumption Finite normal-form games and the Nash map: best-response / Nash continuous map on the product of mixed-strategy simplices has a fixed point that is a mixed Nash equilibrium.
- domain assumption Lean 4 / mathlib foundations (type theory, classical or constructive fragments used) correctly interpret the formalized statements as the intended mathematical theorems.
invented entities (1)
-
BrouwerBench (80-item Lean-grounded benchmark)
Cite this review
Pith. "Pith review of Formalizing Scarf, Brouwer, and Nash in Lean." pith.science (2026). https://pith.science/paper/OFJZE2E7
@misc{pith2026260705987,
author = {Pith},
title = {Pith review of: Formalizing Scarf, Brouwer, and Nash in Lean},
year = {2026},
howpublished = {\url{https://pith.science/paper/OFJZE2E7}},
note = {Machine review of arXiv:2607.05987}
}
read the original 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.
Reference graph
Works this paper leans on
- [1]
-
[2]
Rida Laraki and Jérôme Renault and Sylvain Sorin , title =. 2019 , publisher =. doi:10.1007/978-3-030-26646-2 , isbn =
- [3]
-
[4]
Handbook of Mathematical Economics , editor=
The Computation of Equilibrium Prices: An Exposition , author=. Handbook of Mathematical Economics , editor=. 1982 , publisher=
work page 1982
- [5]
-
[6]
Moura, Leonardo de and Ullrich, Sebastian , booktitle=. The. 2021 , organization=
work page 2021
- [7]
-
[8]
Zheng, Kunhao and Han, Jesse Michael and Polu, Stanislas , booktitle=. 2022 , url=
work page 2022
Show all 10 references
-
[9]
arXiv preprint arXiv:2009.03393 , year=
Generative Language Modeling for Automated Theorem Proving , author=. arXiv preprint arXiv:2009.03393 , year=
2009 arXiv
-
[10]
1985 , publisher=
Fixed Point Theorems with Applications to Economics and Game Theory , author=. 1985 , publisher=
1985
Reviewed July 8, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.