Bollobás–Nikiforov conjecture

Lineage and corrections

Bollobás–Nikiforov conjecture parent of this event

The work claims a complete proof of the original Bollobás–Nikiforov conjecture for every finite non-complete simple graph. More precisely, the Lean theorem `BN.lambda1_sq_add_lambda2_sq_le` proves $$\lambda_1(G)^2+\lambda_2(G)^2 \le 2\left(1-\frac{1}{\omega(G)}\right)|E(G)|.$$ The development proves a stronger weighted spectral inequality. If $B$ is a real symmetric entrywise nonnegative matrix with zero diagonal, supported on the edges of $G$, and $F(B)$ is the sum of the squares of its two largest positive eigenvalues, then $$F(B) \le \left(1-\frac{1}{\omega(G)}\right)\|B\|_F^2.$$ The human-readable manuscript is still preliminary and is being rewritten and polished. parent of this event

VibeMathed record: Bollobás–Nikiforov conjecture evidence for this event

Bollobás–Nikiforov conjecture evidence for this event

Palomar formalization record evidence for this event

MathDB problem record evidence for this event

Original Bollobás–Nikiforov paper evidence for this event

Challenge.lean: the five statements against plain Mathlib, at the reviewed commit evidence for this event

Solution.lean: the comparator-checked bridge to the development evidence for this event

VERIFICATION.md: the recorded comparator and nanoda run evidence for this event

This event attributed to GPT-6 Astra

This event attributed to Grok 4.6

This event attributed to Claude Fable 5.1

This event attributed to Gabriel Coutinho

This event attributed to Yinchen Liu

This event attributed to Thomás Jung Spier

This event attributed to Quanyu Tang

This event attributed to Shengtong Zhang