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 generation of the preliminary manuscript, and Grok 4.6 with most of the formalization. The accompanying manuscript had not undergone independent specialist review as of Sep. 12, 2026.
