arXiv · 2611.03879
Lemmas and Conjectures in Spectral Graph Theory
Abstract
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 most interesting lemmas that were discovered and proved, the ten most useful lemmas, the ten hardest theorems, simpler proofs of known results (Bollobás--Erdős, Yang--Lu), and the unrefuted conjectures that we find most interesting. All the proofs are gathered in an archive
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Tristan Cazenave. 2026-11-02. Lemmas and Conjectures in Spectral Graph Theory. https://arxiv.org/abs/2611.03879
Cite the original work for its findings. Save a collection to share your selection of sources.