← All papers
Formalizing chip-firing and Riemann--Roch for graphs in Lean 4
math.CO
Jun 15, 2026 · v1
TL;DR
Formalizes the Baker-Norine Riemann-Roch theorem for graphs in Lean 4.
Abstract
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.
Problem
Give a complete machine-checked proof of the Baker-Norine Riemann-Roch theorem for graphs, which establishes an analogy between finite graphs and algebraic curves.
Approach
A complete formalization in Lean 4 covering existence and uniqueness of q-reduced divisors, a modified Dhar's burning algorithm, the bijection between acyclic orientations with unique source and maximal superstable configurations, and Clifford's theorem.
Results
Delivers a complete formal proof of the theorem and records several challenges for future formalization.