Lemmas and Conjectures in Spectral Graph Theory
A corpus of 305,755 automatically generated conjectures relates spectral and metric invariants of connected graphs. Each conjecture needs to be refuted or proved, and the proofs should be machine-checked.
A pipeline built with Claude Code first tries numerical refutation on a database of graphs. It then attempts proofs with the z3 SMT solver from a library of lemmas, mines new linear lemmas that rule out z3 countermodels, and exports the proofs to Lean 4/Mathlib for SimpleGraph (Fin n). Deep results, including the Yang–Lu Randić index bound, were formalized as a SpectralLean library.
The pipeline refuted 162,964 conjectures and proved 117,390 without unproved hypotheses; 79,505 of these are verified end to end in Lean. The Yang–Lu formalization uncovered several gaps in the original paper. Shorter proofs of known results, such as the Bollobás–Erdős bound, emerged from the formalization.
| Lemma | Statement | Proofs | Lean |
|---|---|---|---|
| rad_dia_pos | rad ≥ 1, dia ≥ 1 | 40,630 | ✓ |
| rank_range | 2 ≤ rk(A) ≤ n | 40,451 | ✓ |
| rad_dia | rad ≤ dia ≤ 2 rad | 40,124 | ✓ |
| yang_lu | R ≥ dia/2 + √2 − 1 | 12,949 | ✓ |