A proof of the Bollobás–Nikiforov conjecture in Lean

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

Palomar Registrypalomar/PALOMAR-2026-09-07-000002Sep 7, 2026math.COscore 0

A complete Lean 4 / Mathlib formalization of the Bollobás–Nikiforov conjecture (2007) and of the matrix theorems that prove it. Let G be a finite simple graph with adjacency eigenvalues lambda_1 >= lambda_2 >= ..., m edges and clique number omega(G). The conjecture states that every noncomplete graph on at least two vertices satisfies lambda_1^2 + lambda_2^2 <= 2 (1 - 1/omega(G)) m. The formalization proves it (BN.lambda1_sq_add_lambda2_sq_le) as a consequence of a weighted spectral inequality: for every symmetric entrywise nonnegative matrix B with zero diagonal supported on the edges of G,…

SourceRepositoryJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-07-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-07-000002/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-07-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'