Formalizing chip-firing and Riemann--Roch for graphs in Lean 4
We formalize chip-firing games and the Riemann-Roch theorem on graphs, enabling structured proofs and machine-driven research exploration.
Jun 16, 2026
Support Tokens, Stability Margins, and a New Foundation for Robust LLMs
Reading causal self-attention as a probabilistic model surfaces a barrier constraint, a stability margin analogous to an SVM's, and the support tokens that sit on it. The training change is one log-barrier penalty added to cross-entropy.
Feb 25, 2026