{"id":"arxiv/2606.16679","url":"https://arxiv.org/abs/2606.16679","tags":["math.CO"],"score":0,"title":"Formalizing chip-firing and Riemann--Roch for graphs in Lean 4","domain":"math.CO","source":"arxiv","authors":["Dhyey Dharmendrakumar Mavani","Nathan Pflueger"],"reviews":0,"subject":"math.CO","summary":"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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-06-15","reactions":{}}