Lemmas and Conjectures in Spectral Graph Theory

Setting and notation

All graphs are simple, undirected and connected, with $n \ge2$ vertices and $m$ edges. We write $d_v$ for the degree of $v$, $\Delta$ and $\delta$ for the maximum and minimum degrees, $u \sim v$ for adjacency, $\operatorname{dist}$ for the distance, $\operatorname{ecc}(v) = \max_w \operatorname{dist}(v,w)$, $\operatorname{rad} = \min_v \operatorname{ecc}(v)$ for the radius and $\operatorname{diam} = \max_v \operatorname{ecc}(v)$ for the diameter.

• $A$ is the adjacency matrix, with eigenvalues $\lambda_1 \ge\lambda_2 \ge\cdots\ge\lambda_n$ (counted with multiplicity) and rank $\operatorname{rk}(A)$.

• $L = D - A$ is the Laplacian, with eigenvalues $\mu_1 \ge\mu_2 \ge\cdots\ge\mu_n = 0$.

• $R = \sum_{uv \in E}(d_u d_v)^{-1/2}$ is the Randić index.

We shall freely use the following classical facts.

(F1) Rayleigh: $\lambda_1 = \max_{x \ne0} \frac{x^{\mathsf{T}} A x}{x^{\mathsf{T}} x}$. Courant–Fischer: for a symmetric matrix $M$ with eigenvalues $\nu_1 \ge\nu_2 \ge\cdots$, we have $\nu_2 = \max_{\dim U=2} \min_{z \in U \setminus\{0\}} \frac{z^{\mathsf{T}} M z}{z^{\mathsf{T}} z}$.

(F2) Perron–Frobenius: since $G$ is connected, $\lambda_1 > 0$ is simple and has an eigenvector with all coordinates strictly positive.

(F3) Traces: $\sum_i \lambda_i = \operatorname{tr} A = 0$, $\sum_i \lambda_i^2 = \operatorname{tr} A^2 = 2m$ and $\sum_i \mu_i = 2m$.

(F4) Quadratic form: $z^{\mathsf{T}} Lz = \sum_{uv \in E}(z_u-z_v)^2$.

(F5) $\lambda_1 \le\Delta\le n-1$ and $m \ge n-1$, with equality if and only if $G$ is a tree.

(F6) Smith [8]: if $G$ is complete, then $\lambda_2 = -1$, $\lambda_1 = n-1$, $\operatorname{rk}(A) = n$ and $R = n/2$; otherwise $G$ contains an induced $P_3$ and, by interlacing, $\lambda_2 \ge\lambda_2(P_3) = 0$.

Status of the results. The label (verified in Lean) means that the statement is a Lean 4 theorem proved for every connected graph SimpleGraph (Fin n). This theorem depends only on the standard axioms (propext, Classical.choice, Quot.sound) and contains no sorry. The proofs below are mathematical transcriptions of the formal proofs.

Discovered and proved lemmas

The lemmas of this section were discovered automatically. On a database of 281,672 graphs (all connected graphs with at most 9 vertices, plus extremal families), we searched for linear inequalities between two invariants that ruled out the abstract countermodels returned by z3. They were then proved.

Laplacian and adjacency: $\mu_2 \ge\lambda_2 + 1$

Proof. If $n = 2$, then $G = K_2$, $\lambda_2 = -1$ and $\mu_2 = 0$. Assume $n \ge3$.

Case $\lambda_2 \le0$. It suffices to show $\mu_2 \ge1$. Since $G$ is connected with $n \ge3$, it has a vertex $c$ with two neighbours $a,b$. Let $H$ be the spanning graph with edges $ca,cb$. The spectrum of $L_H$ is $\{3,1,0,\ldots,0\}$. Since $L_G = L_H + L_{G\setminus E(H)}$ and the second term is positive semidefinite, Courant–Fischer gives $\mu_2(G) \ge\mu_2(H) = 1$.

Case $\lambda_2 > 0$. Let $x > 0$ be the Perron vector (F2) and $y$ an eigenvector of $\lambda_2$ orthogonal to $x$. Since $\sum_v x_vy_v = 0$ with $x > 0$ and $y \ne0$, the vector $y$ takes both strictly positive and strictly negative values.

Let $u$ be a vertex where $y$ is maximal ($y_u > 0$), $P = \{v \sim u : y_v > 0\}$ and $d^+ = |P|$. Then

Likewise, if $w$ attains the minimum of $y$ ($y_w < 0$), $N = \{v \sim w : y_v < 0\}$ and $d^- = |N|$, we get $\lambda_2 y_w \ge d^- y_w$, hence $d^- \ge\lambda_2$. In particular $d^\pm\ge1$.

The sets $\{u\} \cup P$ (where $y > 0$) and $\{w\} \cup N$ (where $y < 0$) are disjoint. Set

These vectors have disjoint supports, so they span a plane $U$. For $z = af_1 + bf_2$, we keep in (F4) only the edges $uj$ ($j \in P$) and $wj$ ($j \in N$). These two families of edges are disjoint, because $w \notin P$ and $u \notin N$. On the edge $uj$ we have $z_u - z_j = a(d^+ + 1)$, hence

The Rayleigh quotient is therefore at least $\min(d^+,d^-) + 1$ on $U$. Courant–Fischer then gives $\mu_2 \ge\min(d^+,d^-) + 1 \ge\lambda_2 + 1$. □

Remark. The proof actually establishes the stronger inequality $\mu_2 \ge\min(d^+,d^-) + 1$, where $d^\pm$ are the “signed degrees” at the extremities of an eigenvector of $\lambda_2$. A quick literature search did not find the inequality $\mu_2 \ge\lambda_2 + 1$. A more thorough check is needed before claiming that it is new.

Randić index and spectral radius

The following two classical results serve as tools. They were formalised, which made the corollaries almost immediate.

Proof. With $x_v = \sqrt{d_v}$, we have $x^\top x = 2m$ and $x^\top A x = 2\sum_{uv\in E}\sqrt{d_ud_v}$. Rayleigh gives $S := \sum_{uv\in E}\sqrt{d_ud_v} \le m\lambda_1$. By Cauchy–Schwarz,

• If $t \le0$ and $n = 2$, then $G = K_2$ and $L(\frac{3}{2}t+s) = s - \frac{2}{3} < 1 = m$.

• If $t \le0$ and $n \ge3$, then $L$ and $-L$ are two eigenvalues, so $2L^2 \le2m$. Thus $L(\frac{3}{2}t+s) \le sL \le\sqrt{2m} \le m$, since $m \ge2$.

Remark. The certificate identities were found by a sum-of-squares search and checked symbolically; they are also checked by Lean.

Distances and rank of the adjacency matrix

Proof. Consider the submatrix of $A$ with rows $v_1,\ldots,v_{p-1}$ and columns $v_2,\ldots,v_p$. Its $(i,j)$ entry is $A_{v_i,v_{j+1}}$.

• It equals 1 if $j=i$.

• It is zero if $j>i$, because $v_i$ and $v_{j+1}$ are not adjacent ($j+1 \ge i+2$ and the path is induced).

The submatrix is therefore lower triangular with unit diagonal, of determinant 1, and $\operatorname{rk}(A) \ge p-1$. If $p \ge4$, the vertices $v_1,\ldots,v_4$ induce $P_4$, whose adjacency matrix has determinant 1. An invertible principal submatrix of order 4 gives $\operatorname{rk}(A) \ge4$.

Proof. A geodesic between two vertices at distance $\operatorname{diam}$ is an induced path with $\operatorname{diam}+1$ vertices. Apply Lemma 7.

Proof. If $\operatorname{rad} \le1$, this is immediate since $\operatorname{rk}(A) \ge2$. Otherwise, we use the induced path theorem of Erdős, Saks and Sós (in F. Chung’s proof, which is also formalised): a connected graph of radius $r$ contains an induced path with at least $2r-1$ vertices. Lemma 7 then gives $\operatorname{rk}(A) \ge2r-2$.

Remark. This theorem relates a metric quantity, the radius, to a purely algebraic quantity, the rank. It is attained (zero margin) on the graph database.

The ten most useful lemmas

A proof found by the prover is a minimal (for inclusion) set of library lemmas from which the conjecture follows by nonlinear real arithmetic. We measure the usefulness of a lemma by the number of these proofs that use it, among the 117,390 conjectures proved without any unproved hypothesis. The hypothesis $n \ge2$ of the setting, which appears in 7,670 proofs, is not counted as a lemma.

	Name	Statement	Proofs	Lean
1	rad_dia_pos	$\operatorname{rad} \ge1$, $\operatorname{diam} \ge1$	40,630	✓
2	rank_range	$2 \le\operatorname{rk}(A) \le n$	40,451	✓
3	rad_dia	$\operatorname{rad} \le\operatorname{diam} \le2\operatorname{rad}$	40,124	✓
4	rank_dia	$\operatorname{rk}(A) \ge\operatorname{diam}$, and $\operatorname{rk}(A) \ge4$ if $\operatorname{diam} \ge3$	28,147	✓
5	randic_n	$\sqrt{n-1} \le R \le n/2$	24,731	✓
6	R_pos	$R > 0$	20,614	✓
7	yang_lu	$R \ge\operatorname{diam}/2 + \sqrt{2} - 1$	12,949	✓
8	rad_n	$2\operatorname{rad} \le n$	9,545
9	dia_n	$\operatorname{diam} \le n-1$	8,374	✓
10	m_bounds	$n-1 \le m \le n(n-1)/2$	6,524	✓

The most used lemmas are elementary. They mostly serve to rule out degenerate cases (small graphs, zero values, signs) in inequalities whose core lies elsewhere. Among the deep lemmas, the theorem of Yang and Lu clearly dominates: it occurs in 12,949 proofs, and in the proof of 2,301 of the 2,906 theorems that require a research-level result (§ 5). Next come $R \ge(\lambda_1+1)/2$ (Corollary 4, 550 proofs), $R \ge\lambda_2/2+\sqrt{2}$ (Theorem 6, 544), $\operatorname{rad} \le\operatorname{rk}(A)/2+1$ (Theorem 9, 478) and $\mu_2 \ge\lambda_2+1$ (Theorem 1, 105).

Lemma 10 (rad_dia_pos, verified in Lean). $\operatorname{rad} \ge1$ and $\operatorname{diam} \ge1$.

Proof. Since $n \ge2$, every vertex $v$ has another vertex $w$, and $\operatorname{dist}(v,w) \ge1$. Hence $\operatorname{ecc}(v) \ge1$ for every $v$.

Lemma 11 (rank_range, verified in Lean). $2 \le\operatorname{rk}(A) \le n$.

Proof. The upper bound is obvious. Since $G$ is connected with $n \ge2$, it has an edge $uv$. The principal submatrix of $A$ on $\{u,v\}$ is $\begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}$, of determinant $-1$. Hence $\operatorname{rk}(A) \ge2$.

Lemma 12 (rad_dia, verified in Lean). $\operatorname{rad} \le\operatorname{diam} \le2\operatorname{rad}$.

Proof. $\operatorname{rad}$ is a minimum and $\operatorname{diam}$ a maximum of the same eccentricities. If $c$ attains the radius, the triangle inequality gives $\operatorname{dist}(u,v) \le\operatorname{dist}(u,c) + \operatorname{dist}(c,v) \le2\operatorname{rad}$ for all $u,v$.

Lemma 13 (rank_dia, verified in Lean). $\operatorname{rk}(A) \ge\operatorname{diam}$, and $\operatorname{rk}(A) \ge4$ if $\operatorname{diam} \ge3$.

Proof. This is Corollary 8.

Lemma 14 (randic_n, verified in Lean). $\sqrt{n-1} \le R \le n/2$.

Proof. This is Corollary 5. The lower bound is due to Bollobás and Erdős [4]; the shorter proof given here is discussed in § 6.

Lemma 15 (R_pos, verified in Lean). $R > 0$.

Proof. $G$ has at least one edge and every edge contributes $(d_ud_v)^{-1/2} > 0$.

Lemma 16 (yang_lu, Yang–Lu [6], verified in Lean). $R \ge\frac{\operatorname{diam}}{2}+\sqrt{2}-1$.

Proof. See § 6, which describes the formalised proof and how it differs from the one in the paper.

Lemma 17 (rad_n). $2\operatorname{rad} \le n$.

Proof. Let $T$ be a spanning tree of $G$; distances in $T$ bound those of $G$ from above. Let $P=p_0p_1\cdots p_D$ be a longest path of $T$ and $c=p_k$ with $k=\lceil D/2\rceil$. Let $w$ be a vertex, $p_j$ the first vertex of $P$ met by the path of $T$ from $w$ to $c$, and $h=\operatorname{dist}_T(w,p_j)$.

• If $j \le k$, the path $w \to p_j \to p_D$ has length $h + D - j \le D$, so $h \le j$ and $\operatorname{dist}_T(w,c) = h + k - j \le k$.

• If $j \ge k$, the path $w \to p_j \to p_0$ has length $h+j \le D$, so $\operatorname{dist}_T(w,c) = h+j-k \le D-k \le k$.

Thus $\operatorname{rad} \le\operatorname{ecc}_G(c) \le\operatorname{ecc}_T(c) \le\lceil D/2\rceil\le\lceil(n-1)/2\rceil\le n/2$.

Proved conjectures of the corpus

Here is a selection of conjectures of the corpus, identified by their number, that follow from the previous results.

Proof. (a) This is Theorem 1.

(b) If $\lambda_2 \ge0$, Theorem 6 gives $R^2 \ge\left(\frac{2}{3}\lambda_2+\sqrt{2}\right)^2 = \frac{4}{9}\lambda_2^2+\frac{4\sqrt{2}}{3}\lambda_2+2 \ge\lambda_2+2$. If $\lambda_2 < 0$, the graph is complete (Smith), so $\lambda_2=-1$ and $R=n/2 \ge1$.

(c) Use Theorem 2 and $\operatorname{diam} \le n-1 \le m$.

(d) We have $2\mu_2 \le\mu_1+\mu_2 \le\sum_i \mu_i=2m$, so $\mu_2 \le m \le\lambda_1R$.

(e) Yang and Lu proved $R \ge\frac{1}{2}\operatorname{diam}+\sqrt{2}-1$, which gives $\operatorname{diam} \le2R$. With $\operatorname{diam} \le2\operatorname{rad}$, we get $\operatorname{diam} \le\frac{1}{2}\operatorname{diam}+\operatorname{rad} \le R+\operatorname{rad}$. The theorem of Yang and Lu is itself formalised in Lean (Spectral.L_yang_lu, about 3,500 lines, without sorry). The formal proof keeps the minimal counterexample strategy of the paper, but replaces its second half with a different argument. A strong induction on the number of edges first shows that a non-essential vertex of a minimal counterexample has degree at least 9. It then shows that degrees grow exponentially with the distance to the set of essential vertices. Finally, a diametral geodesic is cut into pieces, each of weight at least $\ell/2+1$ thanks to a local version of Lemma 1 of the paper. The formalisation uncovered several gaps in the paper: a false equivalence about essential vertices (counterexample: $C_5$ plus a pendant vertex), an unproved diameter inequality in Corollary 4, hypotheses of Lemma 6 that are never checked, an incomplete block structure, and index errors in Claims A and B.

(f) First $\lambda_1 \le\Delta$: if $Ax=\lambda_1x$ and $u$ maximises $|x_u|$, then $\lambda_1|x_u| = \left|\sum_{v\sim u}x_v\right| \le d_u|x_u| \le\Delta|x_u|$. Next, let $v$ be a vertex of degree $\Delta$, $w$ any vertex, $k=\operatorname{dist}(v,w)$ and $v=p_0,p_1,\ldots,p_k=w$ a geodesic. The vertices $p_2,\ldots,p_k$ are pairwise distinct, distinct from $v$ and not adjacent to $v$ (since $\operatorname{dist}(v,p_i)=i\ge2$). The sets $\{v\}$, $N(v)$ and $\{p_2,\ldots,p_k\}$ are therefore disjoint, so $1+\Delta+(k-1)\le n$. Thus $\operatorname{rad}\le\operatorname{ecc}(v)\le n-\Delta$, and $\lambda_1+\operatorname{rad}\le\Delta+(n-\Delta)=n$.

Remark. (f) remained “open” for the solver only because its library did not contain the lemma $\operatorname{rad} \le n - \Delta$. (c) and (d) were proved only after the theorem of Favaron–Mahéo–Saclé was added. This illustrates how enriching the library brings down entire families of conjectures.

The ten hardest theorems

Criterion. The internal measures of the prover (number of lemmas, computing time) mostly reflect case distinctions on small graphs. The statements that maximise these measures are nested powers such as $\operatorname{rad} \le R^{2\sqrt{\operatorname{rk}(A)}}$, which often have a three-line human proof. We therefore used two more meaningful criteria.

(i) Depth: the theorem does not follow from the elementary and classical lemmas of the library alone (levels 0 to 2). We checked this by rerunning z3 without the research-level lemmas: it then finds a genuine countermodel. Among the 6,651 research-level theorems verified in Lean, 3,679 can in fact be proved without any deep result. There remain 2,906 that require one of Theorems 1, 6, 9 or the theorem of Yang and Lu.

(ii) Optimality: the inequality is attained (with equality) on at least one graph. Among the theorems that satisfy (i) and (ii), we chose the following ten, avoiding variants of the same statement. The first three are verified in Lean in abstract form: the implication from the lemmas is formal, but Smith’s fact (F6) that they use is not yet formalised. The other seven are verified end to end.

Statement	Deep result	Equality
#118503 $\lambda_2 \le2(R-\sqrt{2})$	Th. 6	$P_3$
#709846 $\lambda_2 \le\operatorname{rk}(A)(R-\sqrt{2})$	Th. 6	$P_3$
#2630815 $\lambda_2 \le\operatorname{diam}(R-\sqrt{2})$	Th. 6	$P_3$
#721942 $\lambda_2 \le2\mu_2-1$	Th. 1	$K_2$
#1935857 $\operatorname{diam} \le R^{3/\sqrt{2}}$	Yang–Lu	$K_2$
#1935639 $\operatorname{diam} \le R(\sqrt{2}+\log\operatorname{rad})$	Yang–Lu	$P_3$
#869836 $\operatorname{rad} \le\operatorname{rk}(A)-\log(\operatorname{rad}/2)$	Th. 9	$C_4$
#1396267 $\operatorname{rad} \le2^{\operatorname{rk}(A)-\operatorname{diam}/2}$	Th. 9	$C_4$
#1356167 $\operatorname{rad} \le1+\operatorname{rk}(A)-\operatorname{rad}/2$	Th. 9	$C_4$
#1454913 $\operatorname{rad} \le\operatorname{rk}(A)-\sqrt{\operatorname{rad}}+\sqrt{2}$	Th. 9	$C_4$

In the proofs below, we write $t=\lambda_2$, $k=\operatorname{rk}(A)$, $D=\operatorname{diam}$ and $r=\operatorname{rad}$.

Proof. By Theorem 1 and $\mu_2 \ge0$: $2\mu_2-1=(\mu_2-1)+\mu_2 \ge t$. For $K_2$: $\mu_2=0$ and $t=-1$.

Proof. By Corollary 5, $R \ge\sqrt{n-1} \ge1$; since $3/\sqrt{2}>2$, we have $R^{3/\sqrt{2}} \ge R^2 \ge1$. This settles the case $D=1$. If $D \ge2$, Yang–Lu gives $R^2 \ge\left(\frac{D}{2}+\sqrt{2}-1\right)^2$. Now $\varphi(D)=\left(\frac{D}{2}+\sqrt{2}-1\right)^2-D$ vanishes at $D=2$ and $\varphi'(D)=\frac{D}{2}+\sqrt{2}-2>0$ for $D \ge2$, so $\varphi(D) \ge0$.

Proof. We have $\log r \ge0$. If $D \le2$, Yang–Lu gives $\sqrt{2}R \ge\frac{D}{\sqrt{2}}+2-\sqrt{2}$, and this quantity is $\ge D$ if and only if $D \le2$. If $D \ge3$, then $r \ge D/2>1$, so $r \ge2$ (lemma rad_dia). Consequently $\sqrt{2}+\log r \ge\sqrt{2}+\log2>2.1$, and $R>D/2$ by Yang–Lu, hence $R(\sqrt{2}+\log r)>1.05D$. For $P_3$: $D=2$, $r=1$, $R=\sqrt{2}$.

Proof. If $r \le2$, then $\log(r/2) \le0$ and $k \ge2 \ge r$. If $r \ge2$, Theorem 9 gives $k \ge2r-2$, and $\log(r/2) \le\frac{r}{2}-1 \le r-2$. Hence $k-\log(r/2) \ge r$. For $C_4$: $r=k=2$.

Proof. Since $D \le k$ (lemma rank_dia), we have $k-\frac{D}{2} \ge\frac{k}{2} \ge r-1$ by Theorem 9. Hence $2^{k-D/2} \ge2^{r-1} \ge r$ for every integer $r \ge1$. For $C_4$: $k=D=r=2$.

Proof. This reads $\frac{3}{2}r \le k+1$. If $r=1$, use $k \ge2$. If $r \ge2$, Theorem 9 gives $k+1 \ge2r-1 \ge\frac{3}{2}r$.

Proof. If $r=1$, $k \ge2>2-\sqrt{2}$. If $r \ge2$, $k \ge2r-2$, and it suffices that $r-\sqrt{r} \ge2-\sqrt{2}$. The function $x \mapsto x-\sqrt{x}$ is increasing on $[1,\infty)$ and equals $2-\sqrt{2}$ at $x=2$.

Remark. Once the deep results are available, these proofs are short. The difficulty lies in those results themselves: the formal proof of Yang–Lu has about 3,500 lines, and $\mu_2 \ge\lambda_2+1$ needs a two-dimensional Courant–Fischer argument. This is also why enriching the library brings down entire families of conjectures.

Simpler proofs of known results

The formalisation led us to replace some proofs from the literature with arguments that are shorter, or easier to make rigorous. We do not know whether these arguments already appear in the literature.

The lower bound of Bollobás and Erdős

Bollobás and Erdős [4] proved that $R \ge\sqrt{n-1}$ for every connected graph, with equality for stars. Their proof determines the minimum by an extremal analysis. The proof of Corollary 5 uses only two classical spectral inequalities and fits in three lines.

Short proof. Set $q=2m-n+1>0$. Favaron–Mahéo–Saclé (Theorem 2) and Hong (Theorem 3) give $m^2<\lambda_1^2R^2 \le qR^2$. On the other hand, $m^2-(n-1)q=(m-n+1)^2 \ge0$. Hence $(n-1)q \le qR^2$.

The equality case can be read off the proof: it requires $m=n-1$ (a tree) and $\lambda_1^2=2m-n+1=n-1$, which characterises the star. This proof was not written by a human. The agent in charge of formalising the lemma reused the two theorems the library already contained, instead of following the original proof. Lemmas formalised earlier thus make later ones almost free.

The theorem of Yang and Lu

Yang and Lu [6] prove $R\ge\operatorname{diam}/2+\sqrt{2}-1$ by considering a minimal counterexample. The first half of their proof (vertex deletions, “essential” vertices) is kept. The second half, which relies on Lemmas 4, 6 and 7, a block structure read off figures, and Claims A and B, is replaced with a shorter argument that needs no analysis of figures. Here are its steps; we write $c=\sqrt{2}-1$ and $f(G)=R-\operatorname{diam}/2$.

1. Weak deletion (replaces Lemma 2 and its orientations). Let $v$ be a vertex, and $d'$ the degrees in $G-v$. If, for every neighbour $u$ of $v$ of degree $d_u\ge2$,

then $R(G-v)\le R(G)$. The proof is a simple term-by-term comparison, using the numerical inequality $2(d-1)(1/\sqrt{d-1}-1/\sqrt{d})\le1/\sqrt{d}$. This condition is automatically satisfied if $d_v\le4$.

2. Minimal counterexample. We choose a counterexample $G$ with as few edges as possible, on a fixed vertex set (a deleted vertex stays isolated, which changes neither $R$ nor $\operatorname{diam}$). All reductions are then spanning subgraphs, and a single induction on the number of edges suffices. We show that the essential vertices lie on a diametral geodesic $P$, that the edges between essential vertices are bridges, that $G-e$ has only two components for an inner essential edge $e$, and that the inner essential vertices have degree at least 3.

3. Degree of the non-essential vertices of $G$ (replaces the five cases of Lemma 3). Every non-essential vertex has degree at least 9. Indeed, a vertex of minimum degree $\delta\le8$ would satisfy the weak deletion condition, thanks to three inequalities that are affine in $d_u$ and checked at their smallest value.

4. Exponential growth (replaces Claim A and its layers). By strong induction on the distance $r$ to the set of essential vertices, a vertex at distance $\ge r$ has degree $\ge g(r)$, where $g(1)=9$, $g(2)=19$ and $g(r)=4g(r-2)-3$, so that $g(r)\ge2^{r+2}+1$.

5. Cutting into pieces (replaces the block structure and Claim B). The inner essential vertices cut $P$ into segments of lengths $\ell_i$, with $\sum\ell_i=\operatorname{diam}$. To each segment we associate the set $I_i$ of non-essential vertices joined to it without going through an essential vertex. These sets are disjoint, and two consecutive segments are never both empty. A local version of Lemma 1 of the paper,

and step 4 give each nonempty piece a weight of at least $\ell_i/2+1+c$. An elementary count concludes: $R\ge\sum_i\ell_i/2+c=\operatorname{diam}/2+c$, which contradicts $f(G)<c$. The formalisation also uncovered several gaps in the paper.

• The equivalence claimed for essential vertices is false (counterexample: $C_5$ plus a pendant vertex). Only the true implication is used.

• Corollary 4 assumes $\operatorname{diam}(G-uw)\le\operatorname{diam}(G)+1$ without justification. We use instead $\operatorname{diam}(G-uw)\ge\operatorname{diam}(G)+1$, which directly contradicts minimality.

• The hypotheses of Lemma 6 are never checked.

• The “pendant” components of $G-e$ are ignored by the block structure. They are handled by an additional deletion lemma.

• The indices in Claims A and B are wrong, and the final inequality, “easy to check by computation”, is not proved.

The complete plan, with all the numerical inequalities, is included in the archive, in the file documents/yang_lu_plan_de_preuve.md.

The most interesting unrefuted conjectures

All the conjectures below were tested:

• on all connected graphs with at most 9 vertices;

• on structured families up to $n = 2000$ (complete $k$-ary trees, hypercubes, random regular graphs, grids, spiders, dumbbells…);

• on closed-form families (paths, cycles, stars, $K_n$, $K_{a,b}$) up to $n = 10^{15}$.

Conjecture 1 and Conjecture 7 were also tested on the 11.7 million connected graphs with 10 vertices.

These tests are not superfluous. Among the 16,630 conjectures that the prover left open, 2,480 turned out to be false on large graphs. For example, $R \le\operatorname{diam} \cdot\mu_1$ (#799714) is false for the complete binary tree with 255 vertices ($R \approx116.1$ whereas $\operatorname{diam} \cdot\mu_1 \approx78.6$).

Conjecture 1 (#643). $R \ge\lambda_2 + 1$.

For two cliques $K_k$ joined by an edge, $R - \lambda_2 - 1 \to0$ (0.012 for $k = 80$). The conjecture would therefore be tight. Theorems 2 and 6 are not enough: the relaxation “traces + Hong + $m \ge n$” has numerical countermodels ($m = n = k + 2$, $\lambda_1 = \lambda_2 = \sqrt{k}$ for $k > 4$). On the other hand, the conjecture holds for all bipartite graphs, in particular for trees (Theorem 31): it remains open for non-bipartite graphs. We propose two strengthenings, with no counterexample up to $n = 10$:

The second implication follows from Theorem 2.

Conjecture 2 (#20829). $\lambda_2 \le\mu_1 - 2$.

It is asymptotically tight on paths ($\lambda_2 \to2$, $\mu_1 \to4$). Theorem 1 only gives $\lambda_2 \le\mu_2 - 1 \le\mu_1 - 1$.

Conjecture 3 (#501193). $2R \le\operatorname{rk}(A) \cdot\lambda_1$.

Equality holds for all complete bipartite graphs $K_{a,b}$ ($\operatorname{rk}(A)=2$, $\lambda_1=R=\sqrt{ab}$). It is an elegant statement relating rank, spectral radius and Randić index. Note that $R\le\lambda_1$ is false in general (paths), so the rank is indispensable.

Archive of the proofs

All the proofs are collected in the archive: https://www.lamsade.dauphine.fr/~cazenave/papers/preuves_spectrales.zip, which contains:

• index_conjectures.csv: one line per conjecture of the corpus (305,755), with its status, its statement, the lemmas of its proof, the counterexample if any and, for the 79,505 verified proofs, the corresponding Lean file and theorem;

• lemmes.csv: the library of lemmas, with statement, reference, Lean theorem and number of proofs that use each lemma;

• lean/: the complete Lean 4 project (the SpectralLean library, including the proof of Yang–Lu) and the 3,650 proof files, with a script that recompiles them all;

• documents/: this report and the detailed plan of the proof of Yang–Lu;

• prouveur/: the code of the pipeline (refutation, proof by z3, lemma mining, Lean export).

The file names and column headers of the archive are in French (LISEZMOI.md is the README). For each verified conjecture #i, the theorem gi states the inequality for every connected simple graph on Fin n. To trust it, it suffices to read the definitions of the invariants (SpectralLean/Invariants.lean) and its statement.

Summary in figures

Conjectures in the corpus	305,755
Refuted	162,964
Proved without any unproved hypothesis	117,390
of which verified end to end in Lean	79,505
Proved under an empirical lemma or an open conjecture	3,798
Undefined on some graphs	7,453
Open and unrefuted (after tests on large graphs)	14,150