{"id":"arxiv/2611.03879","url":"https://arxiv.org/abs/2611.03879","tags":["math.CO"],"score":0,"title":"Lemmas and Conjectures in Spectral Graph Theory","domain":"math.CO","source":"arxiv","authors":["Tristan Cazenave"],"reviews":0,"subject":"math.CO","summary":"The corpus of Elie Duhamel and Tristan Cazenave~\\cite{dc} contains $305{,}755$ automatically generated conjectures relating spectral and metric invariants of connected graphs. A pipeline generated with Claude Code (numerical refutation, proof by the SMT solver \\textsf{z3} from a library of lemmas, discovery of new lemmas, formalisation in \\lean~4/Mathlib) refuted $162{,}964$ conjectures and proved $117{,}390$ without any unproved hypothesis, of which $79{,}505$ are verified end to end in \\lean{} for every connected graph. This document collects, with proofs written for mathematicians, the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-11-02","reactions":{}}