chip-firing-with-lean

Chip-Firing with Lean4

This repository contains a complete formalization of the Riemann-Roch theorem for graphs. It includes the necessary background on chip-firing games on multigraphs, using the Lean 4 theorem prover and the Mathlib library. It loosely follows the terminology and organization of Chapters 1 through 5 of Divisors and Sandpiles by Corry-Perkinson. We hope that this library will serve as the starting point for the formalization of other topics, such as combinatorial Brill--Noether theory, that are build on the divisor theory of finite graphs.

Project documentation (including this project's docs and its Mathlib dependencies) is available at: Chip-Firing with Lean Documentation

Preprint (published in arXiv, under-review at Annals of Formalized Mathematics) is available at: arXiv Preprint

Co-developed by Dhyey Mavani and Nathan Pflueger

Project Structure

This proof of Riemann--Roch is organized into the following files. Two additional files, CFGraphExample.lean and Algorithms.lean, are independent material that are not dependencies for the main theorems.

┌────────────────────────────────────────────────────────────────────────┐
│ Basic.lean                                                             │
│ Divisor groups, winnability,                                           │
│ q-reducedness                                                          │
└────────────────┬──────────────────────────────────────┬────────────────┘
                 │                                      │
┌────────────────┴────────────────┐    ┌────────────────┴────────────────┐
│ Config.lean                     │    │ Rank.lean                       │
│ Configurations, superstability, │    │ Baker-Norine ranks              │
│ Dhar's algorithm                │    │                                 │
└────────────────┬────────────────┘    └────────────────┬────────────────┘
                 │                                      │
┌────────────────┴────────────────┐                     │
│ Orientation.lean                │                     │
│ Orientations, consequences      │                     │
│ for superstability              │                     │
└────────────────┬────────────────┘                     │
                 │                                      │
┌────────────────┴──────────────────────────────────────┴────────────────┐
│ RRGHelpers.lean                                                        │
│ Helper results for Riemann-Roch                                        │
└───────────────────────────────────┬────────────────────────────────────┘
                                    │
┌───────────────────────────────────┴────────────────────────────────────┐
│ RiemannRoch.lean                                                       │
│ Proof of Riemann-Roch theorem and corollaries; gonality                │
└────────────────────────────────────────────────────────────────────────┘

Installation

Install Lean 4 and Lake: Follow the Lean 4 installation guide.

Clone the Repository:

git clone https://github.com/DhyeyMavani2003/chip-firing-with-lean.git
cd chip-firing-with-lean

Build the Project: Use the Lake build tool to compile and set up dependencies.
```
lake exe cache get
lake build
```

For futher information about working with Lean4/Mathlib projects, consult the Mathlib project guide.

Contact

For questions, contributions, or collaboration, please reach out to Dhyey Mavani and Nathan Pflueger.

Citation Format

@misc{mavani2026formalizingchipfiringriemannrochgraphs,
      title={Formalizing chip-firing and Riemann--Roch for graphs in Lean 4}, 
      author={Dhyey Dharmendrakumar Mavani and Nathan Pflueger},
      year={2026},
      eprint={2606.16679},
      archivePrefix={arXiv},
      primaryClass={math.CO},
      url={https://arxiv.org/abs/2606.16679}, 
}