Bollobás–Nikiforov two-eigenvalue inequality

Does λ₁(G)²+λ₂(G)²≤2(1−1/ω(G))|E(G)| hold for every finite simple noncomplete graph G with at least two vertices? Here λ₁,λ₂ are the largest adjacency eigenvalues and ω is clique number; a related weighted target uses the two largest positive eigenvalues of nonnegative symmetric zero-diagonal matrices.

Why it matters and what counts as progress

Why it matters: Adding the second eigenvalue strengthens the established spectral clique bound and tests a longstanding general graph inequality.

What counts as progress: Prove the inequality for all graphs, extend the weighted version or characterize equality beyond previously solved classes.

How the problem developed

2007 · Conjecture [1]
Béla Bollobás and Vladimir Nikiforov Proposed a sharp inequality relating the largest two adjacency eigenvalues of a graph to its clique number.
2024 · Partial result [2]
Zhang Established the inequality in the regular-graph setting, leaving the general graph case open.
2026 · Proof and formalization [3]
Shengtong Zhang Posted a proof of the weighted two-eigenvalue inequality with a Lean formalization in the associated repository.

AI contribution

The Bollobás–Nikiforov inequality for nonnegative edge weights

Gabriel Coutinho, Yinchen Liu, Thomás Jung Spier, Quanyu Tang, Shengtong Zhang

The authors prove λ₁(G)²+λ₂(G)²≤2(1−1/ω(G))|E(G)| for every finite simple noncomplete graph G with at least two vertices. A stronger weighted theorem bounds the two largest positive eigenvalues of a symmetric nonnegative zero-diagonal matrix supported on G by (1−1/ω(G)) times its squared Frobenius norm.

AI involvementAI-centered

ImportanceMajor

Technical verificationFormal (Lean 4 with Mathlib and Comparator/NanoDa)

Human understandingFew