Skip to content
DraconiticResearch
Search Sources API
201,683 studies31 sourcesUpdated 5 min ago
PreprintCC BY 4.0arXiv

Lemmas and Conjectures in Spectral Graph Theory

  • Tristan Cazenave
Open at sourcePDFDOICite

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

Related

  1. A general theorem in spectral extremal graph theory
    John Byrne, Dheer Noal Desai, Michael Tait
    Transactions of the American Mathematical SocietyPeer-reviewedLicence not statedFull text24 citedCombinatorics & discrete mathematicsGeometry & topologyOpenAlex
  2. Evaluating SU(3) Verlinde sums using spectral graph theory
    Jay Jorgenson, Anders Karlsson, Lejla Smajlović
    arXivPreprintCC BY 4.0Full textAlgebra & number theoryCombinatorics & discrete mathematicsarXiv
  3. Spectral Schwarz Lemmas and Parallel Obstructions to Metric Comparison
    Xu Pang, Yao Sha, Ren Xin-An
    arXivPreprintarXiv licenceFull textAnalysis & PDEsGeometry & topologyarXiv
  4. The Spectral Theory of Cographs: A Survey, Organized by Graph Matrix
    Pallabi Manna, Santanu Mandal, Fernando C. Tura
    arXivPreprintCC BY 4.0Full textCombinatorics & discrete mathematicsarXiv
  5. Proofs of Li, Wang and Guo's conjectures on (signless) Laplacian spectral radius
    Hongzhang Chen, Jianxi Li, Xiaoyun Lv
    arXivPreprintarXiv licenceFull textCombinatorics & discrete mathematicsarXiv

Cite

BibTeXRIS
BibTeX
@misc{cazenave2026lemmas,
  title = {{Lemmas and Conjectures in Spectral Graph Theory}},
  author = {Tristan Cazenave},
  howpublished = {arXiv},
  year = {2026},
  month = nov,
  doi = {10.48550/arxiv.2611.03879},
  eprint = {2611.03879},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2611.03879},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Lemmas and Conjectures in Spectral Graph Theory
AU  - Tristan Cazenave
PY  - 2026
DA  - 2026/11/02
PB  - arXiv
DO  - 10.48550/arxiv.2611.03879
UR  - https://arxiv.org/abs/2611.03879
AB  - 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
ER  -