{"id":"f12a17ac-0b6e-47c0-ac7f-bb2110ca728a","arxiv_id":"2607.05987","paper_version":1,"verdict":"CONDITIONAL","confidence":"LOW","novelty_score":5.5,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Lean 4 formalization of Scarf→Brouwer→Nash via Ivanov’s indexed-order Scarf theorem, grid instantiation, product embedding, and the Nash map, plus an 80-item BrouwerBench.","lead":"The authors machine-check in Lean 4 a full combinatorial path from Scarf’s theorem through Brouwer’s fixed-point theorem to mixed Nash equilibrium existence. A smart generalist might care because it turns classical existence theorems into inspectable, reusable formal artifacts and ships a small proof-structure benchmark.","discovery_kind":"extension","skeptic_critique":{"model":"grok-4.5","headline":"Continuum lift from Scarf grid almost-fixed-points to exact Brouwer, and the product embedding–projection for Nash, remain the load-bearing unverified steps; combinatorial Scarf core is not the weak link.","rationale":"The reader’s weakest_assumption correctly isolates the continuum lift and the product embedding–projection as the fragile steps of the claimed complete route. The combinatorial Scarf core and room–door parity are not the load-bearing risk; they are standard and external. No internal inconsistency is visible from the abstract, and circularity is low because the targets are classical theorems. The contribution is the formalization artifact (plus BrouwerBench), so soundness turns on whether the Lean development actually closes those two analytic steps without gaps or sorries. Neither this pass nor the reader executed the code, so formal_verification remains none and confidence stays low. CONDITIONAL with medium correctness_risk is therefore still the right call; a clean build-and-statement check would move the verdict toward ACCEPT. No deeper objection (e.g., wrong theorem statement by design, or circular use of Nash) is supported by the available text.","tokens_in":2091,"tokens_out":710,"duration_ms":34405,"concrete_test":"Obtain the paper’s Lean 4 repository. Run lake build; grep the continuum-lift and product-embedding modules for sorry/axiom. Check that the formalized Brouwer statement is equivalent to ∀ f : C(stdSimplex ℝ (Fin (n+1)), stdSimplex ℝ (Fin (n+1))), ∃ x, f x = x (Mathlib form) with no extra hypotheses, and that the product theorem’s fixed-point transfer lemma is stated and proved without sorry. If build is clean and both statements match classical form, the concern does not land; any sorry or weakened statement confirms the gap.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Central claim is a complete Lean 4 route Scarf→Brouwer→Nash. Combinatorial Scarf (Ivanov indexed order, room–door incidence, parity) is classical and, if formalized, likely solid. The load-bearing condition is the continuum step: for continuous f:Δ→Δ, grid almost-fixed-points x_k with ||f(x_k)−x_k||<ε_k, ε_k→0, must yield an exact fixed point via compactness of Δ and continuity of f. In Lean this requires correct Mathlib topology on the standard simplex, a complete sequential/filter compactness argument, and a final Brouwer statement that is the classical continuous map theorem with no residual discreteness hypotheses. The abstract asserts they “carry out the compactness and continuity argument”; that carrying-out is the single place the completeness claim can fail without being obvious from the combinatorial setup. Secondary but still load-bearing for Nash: the explicit embedding–projection e:∏Δ^{n_i}↪Δ^N, p:Δ^N→∏Δ^{n_i} must conjugate fixed points of the lifted map back to fixed points of the Nash map on the product; a mismatch in the conjugate (or a gap in the product Brouwer statement) breaks the Nash existence theorem even if single-simplex Brouwer is correct. Neither step is settled by the abstract alone.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","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.","tokens_in":2343,"tokens_out":343,"duration_ms":7220,"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":[{"comment":"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).","section":null},{"comment":"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.","section":null}],"minor_comments":[],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":{"model":"grok-4.5","summary":"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.","responses":[{"response":"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_made":"yes","referee_comment":"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)."},{"response":"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_made":"yes","referee_comment":"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."}],"tokens_in":1468,"tokens_out":788,"duration_ms":21341,"standing_objections":[]},"desk_editor":{"model":"grok-4.5","letter":"The one thing worth knowing: this is a Lean formalization paper, not a new existence theorem. If the development compiles end-to-end without sorries, you get a reusable combinatorial path from Ivanov’s Scarf through Brouwer to mixed Nash, plus a small 80-item Lean-grounded benchmark. That is useful inside interactive theorem proving and formalized game theory; it does not change applied equilibrium computation.\n\nWhat is actually new is the full Lean 4 development of that known route: room–door incidence and parity for Scarf, instantiation on finite grids of the simplex, the compactness–continuity lift to a continuous fixed point, the explicit embedding–projection that extends Brouwer to products of simplices, and the Nash map. Classical targets, classical combinatorial spine (Ivanov). Credit where it is earned: finishing that path in Lean 4 and packaging BrouwerBench is real work. Machine-checked proofs, if present and public, are the right kind of evidence and should be weighted as such.\n\nSoft spots match the stress test and are load-bearing rather than cosmetic. The combinatorial Scarf core is unlikely to be the weak link. The continuum step—grid almost-fixed-points with ||f(x_k)−x_k||→0, plus compactness of Δ and continuity of f, yielding an exact Brouwer fixed point with no residual discreteness—has to be done cleanly against Mathlib topology. Same for the product embedding–projection conjugating fixed points back for the Nash map. The abstract asserts both; without a green build and a look at those lemmas I cannot confirm they close. That is a verification gap, not a reason to invent deeper flaws. Circularity is low; the targets are external classical theorems.\n\nWho it is for: people who care about formalized fixed-point theory, Lean libraries for topology or game theory, and small structure-aware benchmarks. A serious referee who will check the Lean code, not just the prose, is the right next step. I would send it to peer review rather than desk-reject; accept-or-revise turns on whether the continuum and product steps are actually complete. Engage if you work in ITP or formalized economics; otherwise skim and wait for the artifact.","headline":"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.","tokens_in":3054,"tokens_out":576,"would_cite":false,"duration_ms":22638,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68V20","55M20","91A10"],"pacs":[],"model":"grok-4.5","headline":"A complete Lean 4 formalization traces Scarf’s combinatorial theorem through Brouwer fixed points to mixed Nash equilibria in finite games.","keywords":["Lean 4","Scarf's theorem","Brouwer fixed-point theorem","Nash equilibrium","formal verification","combinatorial topology","game theory","proof assistant"],"falsifier":"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.","tokens_in":2892,"feed_emoji":"♟️","tokens_out":1008,"duration_ms":44693,"temperature":0.7,"pith_summary":"This paper builds a fully machine-checked path in Lean 4 from Scarf’s theorem to Brouwer’s fixed-point theorem and then to the existence of mixed Nash equilibria for finite games. It follows Ivanov’s indexed-order formulation of Scarf, formalizes the room–door incidence structure and parity argument, applies the result to finite grids inside the standard simplex, and lifts the discrete almost-fixed points to a continuum fixed point by compactness and continuity. The authors next extend the fixed-point result from one simplex to a finite product of simplices by an explicit embedding–projection construction, then feed that product theorem into the classical Nash map. As a secondary product they extract BrouwerBench, an 80-item Lean-grounded benchmark that probes whether a system understands the internal proof structure of this single development. A sympathetic reader cares because the work turns a classical existence chain that is usually left as informal prose into an inspectable, reusable formal object.","feed_headline":"Lean 4 runs Scarf all the way to mixed Nash equilibria","feed_subtitle":"A combinatorial formalization lifts grids to Brouwer fixed points, products of simplices, and an 80-item proof benchmark.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Lean 4 formalizes Scarf all the way to mixed Nash equilibria","From Scarf theorem to Brouwer and Nash fully in Lean 4","Combinatorial Scarf route yields Brouwer and mixed Nash in Lean 4","Lean 4 lifts Scarf grids to Brouwer fixed points then Nash","Scarf to mixed Nash via full combinatorial proof in Lean 4"],"cache_read_input_tokens":128,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Lean 4 formalizes Scarf all the way to mixed Nash equilibria","From Scarf theorem to Brouwer and Nash fully in Lean 4","Combinatorial Scarf route yields Brouwer and mixed Nash in Lean 4","Lean 4 lifts Scarf grids to Brouwer fixed points then Nash","Scarf to mixed Nash via full combinatorial proof in Lean 4"]},"model":"grok-4.5","cost_usd":0.016422,"raw_usage":{"total_tokens":3255,"prompt_tokens":729,"num_sources_used":0,"completion_tokens":101,"cost_in_usd_ticks":164220000,"prompt_tokens_details":{"text_tokens":729,"audio_tokens":0,"image_tokens":0,"cached_tokens":128},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":2425,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":729,"tokens_out":101,"duration_ms":23828,"temperature":1.0,"reasoning_tokens":2425,"cache_read_input_tokens":128,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-08T19:06:25.349879+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"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.","supporting_citations":[],"review_version":1}