VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
Let $G$ be a finite simple graph with $m=|E(G)|$ edges and clique number $\omega(G)$, and let $\lambda_1(G)\ge\lambda_2(G)\ge\cdots\ge\lambda_n(G)$ be the eigenvalues of its adjacency matrix. Bollobás and Nikiforov conjectured in 2007 that every non-complete graph satisfies $$\lambda_1(G)^2+\lambda_2(G)^2\le 2\Bigl(1-\frac{1}{\omega(G)}\Bigr)m.$$ Before this work it was known for triangle-free graphs (Lin, Ning and Wu), regular graphs (Zhang), graphs with few triangles, complete multipartite graphs, and asymptotically almost surely for random graphs, and open in general.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT-6 Astra; Grok 4.6; Claude Fable 5.1
GPT 6 Astra was used by the five human authors in the ideation and development of the mathematics and generated the preliminary manuscript `docs/sol.tex`.
The resulting proof was then formalized in Lean 4/Mathlib. Grok 4.6 agents in Cursor produced essentially the entire Lean development, working node-by-node from the mathematical proof and a human-directed formalization blueprint. Each component was required to build without `sorry`.
A Claude Fable 5.1 agent subsequently prepared the Palomar submission surface and verification packaging. It did not add substantive proof content.
Lifted from the submitted Lean-checked to Lean-verified, because the correspondence the submitter said nobody had audited was audited here, on 12 September 2026, at commit edb5259. Challenge.lean imports only Mathlib and states the headline theorem entirely in Mathlib vocabulary: $G$ a SimpleGraph on a finite vertex type, $G\ne\top$ for non-complete, Nontrivial for at least two vertices, G.cliqueNum for $\omega$, G.edgeFinset.card for $|E(G)|$ counted once, and $\lambda_1,\lambda_2$ as the first two entries of Mathlib's eigenvalues₀ of the real adjacency matrix, which is nonincreasing. There is no hypothesis beyond those and nothing project-defined in the statement beyond those two thin wrappers, whose definitions sit in the same file. Solution.lean supplies the same five names from the development; comparator.json compares them with only propext, Classical.choice and Quot.sound permitted and with nanoda enabled as an independent kernel; VERIFICATION.md records the comparator run accepting the solution under both kernels; Palomar checks and Lean Action CI passed on GitHub at the reviewed commit. No sorry outside the five deliberate holes in Challenge.lean, no axiom, no native_decide. The build was not repeated here. Candidate rather than Resolved is the site's practice for named conjectures with a formal proof: it flips when a named expert with no stake confirms publicly that the formal statement is the conjecture, a short read since the statement is pure Mathlib.
GitHub repository (Lean 4 proof and preliminary note), pinned to the reviewed commit
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.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
The source status is candidate and must not be represented as solved.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.