Lean4 Machine Assisted Proof Framework for Chip Firing Games & Graphical Riemann-Roch
Lean4 formalization framework for chip-firing gamesAbstract
This paper presents a novel, first-ever Lean4 formalization exploring the interplay between chip-firing games and algebraic geometry, culminating in the graph-theoretic analog of the Riemann–Roch theorem. We focus on the dollar game, a variant of chip firing, for finite and connected graphs. Through a detailed study of chip firing moves and equivalence classes of chip distributions, we investigate key properties such as winnability—whether a given chip configuration can reach a debt-free state through a sequence of legal firing moves. To this end, we analyze and implement efficient algorithms for deciding winnability and characterizing winning strategies. We also examine the graph-theoretic Riemann–Roch theorem introduced by Baker and Norine, establishing a surprising bridge between discrete graph processes and algebraic geometry. We provide an accessible exposition of its statement and proof, leveraging divisor theory and linear equivalence in the context of graphs. A key contribution of this work is developing a formalized proof framework for chip-firing games using the Lean4 proof assistant. By encoding multi-edged graph structures, firing rules, divisors, and related properties within Lean’s theorem-proving environment, we produce verified machine-checked proofs of key results in chip firing and the Riemann-Roch setting assuming a modest set of prerequisites as axioms. This work aims to enhance the Lean4’s existing Mathlib4 library of proofs by providing modularized, formally verified domain content contributing to the growing body of computationally verified mathematics. We also briefly discuss the theoretical and practical implications of agentic-AI frameworks for advancing formal mathematics.
Type
Publication
Lean4 Machine Assisted Proof Framework for Chip Firing Game & Graphical Riemann-Roch
This work introduces Chip-Firing with Lean4, a framework for formalizing chip-firing games on graphs and proving the Riemann-Roch theorem for graphs. Using the Lean4 theorem-proving language, the project provides a modular, proof-assistive environment tailored to graph-theoretic applications.
Project Structure
The codebase is modular with the following key components:
- Basic.lean: Core chip-firing definitions and CFGraph structures
- CFGraph.lean: CFGraph implementation with multi-edge support
- CFGraphExample.lean: Example graphs and chip-firing scenarios for verification
- Config.lean: Configuration-related structures and operations
- Orientation.lean: Orientation definitions and utilities for CFGraphs
- Rank.lean: Rank functions and divisor-related structures
- Helpers.lean: Auxiliary lemmas and general theorems
- RRGHelpers.lean: Specific lemmas for Riemann-Roch theorem proofs
- RiemannRochForGraphs.lean: Main formalization of the Riemann-Roch theorem
Key Features
- Graph Theory Formalization: Provides formal definitions of graphs, chip configurations, and divisors within Lean4’s type system
- Chip-Firing Mechanics: Models chip-firing moves, firing rules, and the dollar game with precise mathematical constructs
- Winnability Analysis: Implements algorithms for determining whether chip configurations can reach debt-free states
- Riemann-Roch Formalization: Establishes and proves the graph-theoretic Riemann-Roch theorem with machine-verified proofs
- Modular Design: Offers reusable lemmas and structures for broader graph-theoretical research
- Visualization Support: Optional integration with Paperproof for enhanced proof visualization
Technical Implementation
The framework leverages:
- Lean 4 theorem prover for formal verification
- Mathlib4 for foundational mathematical structures
- Lake build system for dependency management
- Docker containerization for reproducible environments
Mathematical Contributions
This work bridges discrete mathematics and algebraic geometry by:
- Formalizing the connection between chip-firing games and divisor theory
- Providing machine-verified proofs of key results in the Baker-Norine framework
- Establishing a foundation for future formal mathematics research in combinatorial algebraic geometry
- Contributing verified mathematical content to the Lean4/Mathlib4 ecosystem
