Formalizing chip-firing and Riemann--Roch for graphs in Lean 4

The Riemann–Roch theorem for graphs, due to Baker and Norine, is a foundational result establishing a powerful analogy between finite graphs and algebraic curves. We describe a complete formal proof of this theorem implemented in the Lean 4 theorem prover. Our formalization includes the existence and uniqueness of q-reduced divisors, a modified form of Dhar’s burning algorithm, the bijection between acyclic orientations with unique source and maximal superstable configurations, and Clifford’s theorem. We also include several challenges for future formalization.

Formalizing chip-firing and Riemann–Roch for graphs in Lean 4