A Proof of Graffiti 295:
Positive Distance Eigenvalues and Mean Gravity
We prove Graffiti 295: for every connected simple graph \(G\) of order \(n\) and girth at least five, the number \(n_+(D)\) of positive eigenvalues of the distance matrix, counted with multiplicity, satisfies \[ n_+(D)\;\le\;\frac{n}{\overline{\operatorname{Gr}}}, \] where \(\overline{\operatorname{Gr}}\) is the mean of the gravity matrix. The source does not define the mean of a matrix; the result holds for the mean over all \(n^2\) entries and for the mean over the \(n(n-1)\) off-diagonal entries. The proof is short: for girth at least five both means are at most \(1\), so \(n/\overline{\operatorname{Gr}}\ge n\), and an \(n\times n\) matrix has at most \(n\) eigenvalues. It is machine-checked in Lean 4 with Mathlib, using only Lean's standard axioms, and an exact battery finds no violation on 346 graphs. Novelty is stated provisionally.
1. The conjecture
Let \(G\) be a connected simple graph on \(n\) vertices with \(m\) edges. Its distance matrix \(D\) has entry \(d(u,v)\), the graph distance. Its gravity matrix (Written on the Wall, p. 52) is
where \(d(u)\) is degree. Graffiti 295 (page 80 of Fajtlowicz's Written on the Wall) reads: "If girth is ≥ 5 then the number of positive eigenvalues of the distance matrix ≤ n / meangravity." Conjectures that involve distance are for connected graphs (p. 2). We write \(n_+(D)\) for the number of positive eigenvalues of \(D\), counted with multiplicity. As of September 2024 the conjecture was listed open in Table 1 of Roucairol–Cazenave, after their search algorithms found no counterexample.
2. The proof
Proof. This is §2.5 of the Graffiti 290 paper. Girth at least five gives \(\sum_v d(v)^2\le n(n-1)\), so \((2m)^2\le n\sum_v d(v)^2\le n^2(n-1)\) by Cauchy–Schwarz. Since \(d(u,v)\ge1\) off the diagonal, \(\sum\operatorname{Gr}\le\bigl((2m)^2-\sum_v d(v)^2\bigr)/(n-1)\le(2m)^2/n\). Divide by \(n^2\) or by \(n(n-1)\). ∎
Proof. The characteristic polynomial of \(D\) has degree \(n\), so \(D\) has at most \(n\) eigenvalues and \(n_+(D)\le n\). If \(G\) has an edge, then \(n\ge2\) and the mean gravity is positive, and by Lemma 1 it is at most \(1\). So \(n\le n/\overline{\operatorname{Gr}}\) and \(n_+(D)\le n/\overline{\operatorname{Gr}}\). If \(G\) has no edge, then every distance is \(0\) in Mathlib's convention for vertices that no path joins, so \(D=0\) and \(n_+(D)=0\). This case does not arise for a connected graph with \(n\ge2\); it is covered only because the proof does not use connectivity. ∎
Remark (a margin of more than 2). For connected \(G\) with \(n\ge2\), \(D\) is a nonzero symmetric matrix with trace \(0\), so it has a negative eigenvalue and \(n_+(D)\le n-1\). With \(\overline{\operatorname{Gr}}_{n^2}\le(n-1)/n\) this gives \(n/\overline{\operatorname{Gr}}-n_+(D)\ge n^2/(n-1)-(n-1)=(2n-1)/(n-1)>2\). This remark is not part of the Lean development.
3. Why an earlier attack stalled
Our first attack on 295 (July 23, 2026; output) bounded the right side with Reiman's edge cap, which gives only \(n/\overline{\operatorname{Gr}}\gtrsim n-O(\sqrt n)\). It bounded the left side by \(n_+(D)\le n-\operatorname{diam}(G)\), using a geodesic path, the Graham–Pollak spectrum of a path's distance matrix, and Cauchy interlacing. The two bounds met only for large diameter and for diameter \(2\), and left a gap at intermediate diameter. Subtracting the diagonal in Lemma 1 raises the right side to at least \(n^2/(n-1)>n\), so no bound on the left side beyond \(n_+(D)\le n\) is needed.
4. A machine-checked proof in Lean 4
We formalized the theorem in Lean 4 with Mathlib. Lean's kernel checks every inference. The source is on GitHub at agnt-gg/graffiti-lean (commit daf0f85) and in the archive.
Degree, distance and girth are Mathlib's SimpleGraph.degree, SimpleGraph.dist and SimpleGraph.egirth. The gravity matrix is defined as in the Graffiti 290 paper. As in SimpleGraph.cvetkovic of formal-conjectures, positive eigenvalues are counted with multiplicity as positive roots of the characteristic polynomial. The main statement reads:
noncomputable def distanceMatrix (G : SimpleGraph α) : Matrix α α ℝ :=
Matrix.of fun u v => (G.dist u v : ℝ)
theorem graffiti_295 {α : Type*} [Fintype α] [DecidableEq α] (G : SimpleGraph α)
[DecidableRel G.Adj] (hconn : G.Connected) (hgirth : 5 ≤ G.egirth) :
(G.distanceMatrix.charpoly.roots.countP (fun x => 0 < x) : ℝ) ≤
Fintype.card α / G.meanGravity
| Theorem | Statement |
|---|---|
graffiti_295 | Graffiti 295, with the mean over all \(n^2\) entries of the gravity matrix. |
graffiti_295.variants.off_diagonal_mean | Graffiti 295, with the mean over the \(n(n-1)\) off-diagonal entries. |
Fidelity to the source.
- Distance matrix. Entry \((u,v)\) is
G.dist u v. The matrix is symmetric (isSymm_distanceMatrix), so its characteristic polynomial has \(n\) real roots and the count is the number of positive eigenvalues. - Gravity. On p. 52 an entry is \(0\) when no path joins \(u\) and \(v\). Mathlib's
distis \(0\) for such a pair and Lean defines \(x/0=0\), so the Lean entry is also \(0\). - Connectivity. Conjectures that involve distance are only for connected graphs (p. 2). Hence the hypothesis
G.Connected. - Girth. An acyclic graph has
egirth = ⊤, so it satisfies the girth hypothesis. - Mean. The source does not define the mean of a matrix, so both readings are proved.
What was checked.
- The project builds with
lake buildon Lean v4.33.1 with Mathlib v4.33.1 (commit0df444a), with warnings treated as errors. - For both theorems,
#print axiomsreports onlypropext,Classical.choiceandQuot.sound, Lean's standard axioms. There is nosorry, no custom axiom and nonative_decide. - The definitions and statements are character-for-character identical to the statement file submitted to Google DeepMind's formal-conjectures repository.
- The shared lemmas behind Lemma 1 fail to compile when the girth hypothesis is weakened from 5 to 4, or when the gravity bound is tightened to \((2m)^2/n^2\).
As with any Mathlib proof, this check trusts the Lean kernel and the Mathlib definitions above. Mathlib's prebuilt library files were loaded, not rebuilt from source.
5. Verification
Battery 1 (battery_295.py) computes the gravity sums in exact rational arithmetic and the distance spectra numerically, on 346 connected graphs of girth at least five: 12 named graphs, all 34 with \(n\le7\), and 300 random ones. It finds no violation for either reading of the mean. Battery 2 is the Lean kernel (§4). The positive-eigenvalue counts in Table 2 agree with those of the July attack.
| Graph | n | \(n_+(D)\) | \(n/\overline{\operatorname{Gr}}_{n^2}\) | \(n/\overline{\operatorname{Gr}}_{n(n-1)}\) |
|---|---|---|---|---|
| C₅ | 5 | 1 | 8.333 | 6.667 |
| Petersen | 10 | 1 | 16.667 | 15.000 |
| Heawood | 14 | 7 | 38.606 | 35.848 |
| Hoffman-Singleton | 50 | 22 | 89.286 | 87.500 |
| McGee | 24 | 9 | 140.190 | 134.349 |
| Tutte-Coxeter | 30 | 12 | 241.667 | 233.611 |
| Pappus | 18 | 5 | 72.000 | 68.000 |
| Desargues | 20 | 1 | 94.351 | 89.634 |
| Dodecahedral | 20 | 1 | 94.351 | 89.634 |
| P₁₀ | 10 | 1 | 68.229 | 61.406 |
| K₁,₈ | 9 | 1 | 37.385 | 33.231 |
| K₂ | 2 | 1 | 4.000 | 2.000 |
6. Novelty status — stated provisionally
7. Reproduction protocol
python -m pip install networkx numpy python battery_295.py # 346 graphs, exact rational gravity # Lean (§4): in the lean/ folder of the archive, or a clone of agnt-gg/graffiti-lean lake exe cache get # prebuilt Mathlib lake build # checks the proofs and prints their axioms
Dependencies: Python 3.13, NetworkX 3.5, NumPy 2.3; Lean v4.33.1 and Mathlib v4.33.1, both pinned in the Lean files.
8. Artifact ledger
| Artifact | Purpose |
|---|---|
| agnt-gg/graffiti-lean · archived copy | Lean 4 proof, with the shared definitions and lemmas |
| battery_295.py · output | Exact battery on 346 graphs |
| claim-ledger.json | Claim-by-claim evidence map |
| wow-p80-top.png | Primary source scan of page 80 (conjectures 292 and 295) |
| SHA256SUMS.txt | Integrity ledger |
Principal hash: lean/Graffiti/Graffiti295.lean 6cebb609bb57b7ded54e18adc96eea8651837267e5ef881a4138914951ac149e.
References
- S. Fajtlowicz, "Written on the Wall," July 2004, p. 80 (conjecture 295); p. 52 (gravity matrix definition); p. 2 (connected graphs).
- M. Roucairol and T. Cazenave, "Refutation of Spectral Graph Theory Conjectures with Search Algorithms," arXiv:2409.18626, 2024 (Table 1, open status; §5.2, the gravity matrix of Written on the Wall).
- T. L. Brewster, M. J. Dinneen, and V. Faber, "A computational attack on the conjectures of Graffiti: new counterexamples and proofs," Discrete Mathematics 147 (1995), 35–55.
- R. L. Graham and H. O. Pollak, "On the addressing problem for loop switching," Bell System Technical Journal 50 (1971), 2495–2519.
- AGNT Labs, "A Proof of Graffiti 290" and "A Proof of Graffiti 292," 2026, 290, 292.
- N. Wilbanks and Annie, "graffiti-lean: Lean 4 proofs of Graffiti conjectures 290, 292 and 295," GitHub, 2026, agnt-gg/graffiti-lean, commit daf0f85.
- L. de Moura and S. Ullrich, "The Lean 4 Theorem Prover and Programming Language," Automated Deduction – CADE 28, LNCS 12699 (2021), 625–635.
- The mathlib Community, "The Lean Mathematical Library," Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 367–381.
This is what the product is for
AGNT Labs publishes its working out. The same discipline runs through the product: every agent run produces a receipt showing what it did, what it read, and why — so a result can be checked rather than trusted. AGNT runs on your own machine and is free to use.