The Bollobás-Nikiforov conjecture (Bollobás and Nikiforov 2007) states that if 
is a noncomplete finite simple graph with at least
two vertices, 
is its edge count, 
is its clique number, and the graph
eigenvalues are ordered 
, then
 |
Coutinho et al. (2026) give the following stronger weighted inequality. Let 
be a real matrix that is both a symmetric
matrix and a nonnegative matrix. Suppose
it has zero diagonal and satisfies 
when 
. If 
is the sum of the squares of the two largest positive eigenvalues of 
, then
 |
where 
is the Frobenius norm. Taking 
to be the adjacency matrix
of 
gives the conjectured inequality.
The stronger inequality and the Bollobás-Nikiforov conjecture have been formalized in Lean 4. The development contains no admitted results and uses only the standard Mathlib axioms. The authors credit GPT-6 Astra with mathematical ideation and Grok 4.6 with most of the formalization. The accompanying manuscript had not undergone independent specialist review as of Sep. 12, 2026.
