Chip-Firing with Lean4: A Formalization Framework for Graph Theory
Jan 25, 2025·,·
1 min read
Dhyey Mavani
Professor Nathan Pflueger
Abstract
As part of my final honors thesis in mathematics, this work presents a Lean4-based framework for the formalization of chip-firing games and the Riemann-Roch theorem on graphs. Using structured reasoning and theorem-proving tools, the project introduces a robust foundation for graph theory applications while integrating agentic AI systems to assist mathematicians in transforming proof intuitions into verified formal proofs.
Type
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.
Key Features:
- Graph Theory Formalization: Defines structures like CFGraphs, divisors, and orientations with Lean4.
- Chip-Firing Mechanics: Models chip-firing games and the dollar game with precise mathematical constructs.
- Riemann-Roch Formalization: Establishes and proves the graph-theoretic Riemann-Roch theorem.
- AI-Assisted Proofs: Explores generative AI tools for converting mathematicians’ proof ideas into formalized proofs, accelerating research workflows.