Let (G) be a finite simple graph with (m) edges and clique number (omega(G)). Let lambda_1(G)≥ lambda_2(G)≥ … ≥ lambda_n(G) be the eigenvalues of the adjacency matrix of (G). The Bollobás–Nikiforov conjecture asserts that if (G) is not a complete graph, then lambda_1(G)^2+lambda_2(G)^2 ≤ 2(1-frac1omega(G))m. Equivalently, if (G) is a non-complete (K_r+1)-free graph, then lambda_1(G)^2+lambda_2(G)^2 ≤ frac2(r-1)rm. This conjecture was proposed by Béla Bollobás and Vladimir Nikiforov in their 2007 paper Cliques and the spectral radius. It is a spectral strengthening of Turán-type extremal inequalities and has become a well-known open problem in spectral graph theory. A number of special cases and related strengthenings have been studied in the subsequent literature.

Bollobás–Nikiforov conjecture

Let $G$ be a finite simple graph with $m$ edges and clique number $\omega(G)$ . Let

\lambda_1(G)\ge \lambda_2(G)\ge \cdots \ge \lambda_n(G)

be the eigenvalues of the adjacency matrix of $G$ .

The Bollobás–Nikiforov conjecture asserts that if $G$ is not a complete graph, then

\lambda_1(G)^2+\lambda_2(G)^2 \le 2\left(1-\frac{1}{\omega(G)}\right)m.

Equivalently, if $G$ is a non-complete $K_{r+1}$ -free graph, then

\lambda_1(G)^2+\lambda_2(G)^2 \le \frac{2(r-1)}{r}m.

This conjecture was proposed by Béla Bollobás and Vladimir Nikiforov in their 2007 paper Cliques and the spectral radius. It is a spectral strengthening of Turán-type extremal inequalities and has become a well-known open problem in spectral graph theory.

A number of special cases and related strengthenings have been studied in the subsequent literature.

References

B. Bollobás and V. Nikiforov, Cliques and the spectral radius, Journal of Combinatorial Theory, Series B 97 (2007), 859–865. https://doi.org/10.1016/j.jctb.2006.12.002

L. Liu and B. Ning, Unsolved Problems in Spectral Graph Theory, arXiv:2305.10290.

Posted by Quanyu Tang Posted 1 day ago · edited 19 hours ago

Progress summary

Refreshed 19 hours ago

Claimed solved

A public claim says the conjecture has been fully proved and checked by computer, but independent verification is not yet reported.

Bollobás and Nikiforov proposed this spectral strengthening of Turán’s theorem in 2007, asserting an upper bound for the two largest adjacency eigenvalues of every non-complete graph. The full statement remains unverified despite a recent claimed proof.

Known results and September 2026 claimed proof

Earlier work proves special cases including triangle-free, weakly perfect, regular, sparse-triangle, and almost surely random graphs. [ $K_4$ ]-free dense graphs are also covered asymptotically by a March 2026 preprint.
The same preprint proves the conjecture for complete multipartite graphs and gives a stability theorem for dense [ $K_4$ ]-free graphs, while explicitly leaving sparse, higher-chromatic cases and small graphs open.
On September 7, 2026, Gabriel Coutinho, Yinchen Liu, Thomás Jung Spier, Quanyu Tang, and Shengtong Zhang announced a proof of the full conjecture together with a Lean 4 formalization. The repository is public, but the accompanying paper is in preparation and independent verification is not reported.

Community submission (unverified)

Posted September 11, 2026, a submitted proof claims that the full conjecture has been formalized in Lean 4. It proposes a stronger inequality for nonnegative symmetric matrices with zero diagonal and derives the graph case using the Frobenius norm identity, while acknowledging that the manuscript is preliminary and not peer-reviewed.

Current status (as of September 2026): Special cases are established, while a full proof is publicly claimed and formally formalized but remains unverified.

Sources

Solution 1ProofA complete Lean 4/Mathlib formalization of the Bollobás–Nikiforov conjecture is publicly available. It proves the conjectured bound for every finite non-complete simple graph, via a stronger weighted spectral inequality. The repository contains the Lean source, verification material, and a preliminary human-readable manuscript, which is still being polished.See full solutionHide full solution

A complete formalization of the Bollobás–Nikiforov conjecture has been implemented in Lean 4 using Mathlib.

For a finite simple graph $G$ with $m=|E(G)|$ , clique number $\omega(G)$ , and adjacency eigenvalues

\lambda_1(G)\ge \lambda_2(G)\ge \cdots \ge \lambda_n(G),

the formalized theorem proves that every non-complete graph satisfies

\lambda_1(G)^2+\lambda_2(G)^2 \le 2\left(1-\frac{1}{\omega(G)}\right)m.

Thus the formalization covers the full Bollobás–Nikiforov conjecture, not merely a special class of graphs.

The argument in fact proves the following stronger weighted spectral inequality. Let $B$ be a real symmetric entrywise nonnegative matrix with zero diagonal whose support is contained in the edges of $G$ . If $F(B)$ denotes the sum of the squares of the two largest positive eigenvalues of $B$ , with missing positive eigenvalues replaced by zero, then

F(B) \le \left(1-\frac{1}{\omega(G)}\right)\|B\|_F^2.

Applying this to the adjacency matrix $B=A_G$ gives the Bollobás–Nikiforov inequality because

\|A_G\|_F^2=2m.

The public Lean repository, including the source files, verification information, and the preliminary mathematical writeup, is available at:

https://github.com/ShengtongZhang-alt/BN

The formalization is also registered in Palomar, a registry of Lean-verified mathematical results:

https://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000002&version=1

The project authors are Gabriel Coutinho, Yinchen Liu, Thomás Jung Spier, Quanyu Tang, and Shengtong Zhang.

The human-readable manuscript in the repository is currently a preliminary research note and is being rewritten and polished. Accordingly, this entry records a claimed complete resolution supported by a public Lean formalization; the accompanying exposition has not yet gone through the usual publication and peer-review process.