Math Thesis Defense - Lean4 Machine Assisted Proof Framework for Chip Firing Game & Graphical Riemann-Roch

This thesis presents a novel, first-ever Lean4 formalization exploring the interplay between chip-firing games and algebraic geometry, culminating in the graph-theoretic analog of the Riemann–Roch theorem. We focus on the dollar game, a variant of chip firing, for finite and connected graphs. Through a detailed study of chip firing moves and equivalence classes of chip distributions, we investigate key properties such as winnability—whether a given chip configuration can reach a debt-free state through a sequence of legal firing moves. To this end, we analyze and implement efficient algorithms for deciding winnability and characterizing winning strategies. We also examine the graph-theoretic Riemann–Roch theorem introduced by Baker and Norine, establishing a surprising bridge between discrete graph processes and algebraic geometry. We provide an accessible exposition of its statement and proof, leveraging divisor theory and linear equivalence in the context of graphs. A key contribution of this work is developing a formalized proof framework for chip-firing games using the Lean4 proof assistant. By encoding multi-edged graph structures, firing rules, divisors, and related properties within Lean’s theorem-proving environment, we produce verified machine-checked proofs of key results in chip firing and the Riemann-Roch setting assuming a modest set of prerequisites as axioms. This work aims to enhance the Lean4’s existing Mathlib4 library of proofs by providing modularized, formally verified domain content contributing to the growing body of computationally verified mathematics. We also briefly discuss the theoretical and practical implications of agentic-AI frameworks for advancing formal mathematics.