AI Proof WatchKeep up with AI contributions

The Bollobás–Nikiforov inequality for nonnegative edge weights

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

The authors prove λ₁(G)²+λ₂(G)²≤2(1−1/ω(G))|E(G)| for every finite simple noncomplete graph G with at least two vertices. A stronger weighted theorem bounds the two largest positive eigenvalues of a symmetric nonnegative zero-diagonal matrix supported on G by (1−1/ω(G)) times its squared Frobenius norm.

Sources for this record

What was already known

Nikiforov proved the λ₁-only inequality; Bollobás–Nikiforov conjectured adding λ₂. Prior proofs covered triangle-free, regular, weakly perfect and sparse-triangle graph classes, while Coutinho–Spier–Zhang had weaker constants for general graphs. Giacomelli’s March 2026 arXiv:2603.26379 addressed special cases, not this general weighted theorem.

AI involvement AI-centered

GPT-6 Astra is credited with mathematical ideation in a collaboration with Coutinho, Liu, Spier, Tang and Zhang. Grok 4.6 agents later formalized the proof under Zhang’s statement-level direction. The available exposition does not document a complete human explanation of the weighted mechanism.

GPT 6 Astra is expressly credited with ideation of the central weighted proof in a human collaboration; Grok later formalized it. More autonomous attribution is unsupported.

Importance Major

The weighted theorem implies the longstanding general Bollobás–Nikiforov conjecture and strengthens earlier special-class results.

Limitations

The proof does not establish the proposed inequality for up to ω(G) eigenvalues, and the authors do not separate every central lemma by human or model origin.

Technical verification Formal (Lean 4 with Mathlib and Comparator/NanoDa)

The repository’s dated record reports five theorem statements matched to Challenge, Lean kernel acceptance, standard axioms and a clean build.

Formal checking

clean lake build, axiom report and statement matching to Challenge

Checker
Lean 4 kernel, NanoDa and Comparator
Scope
Bollobás–Nikiforov and weighted, matrix, Gram and conic headline theorems
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

The preliminary note was model-generated and a more human-readable author exposition was still in progress; the available record does not document how fully humans can explain the central weighted proof.

Correction and publication history

2026-10-18 · publication

The weighted theorem implies the longstanding general Bollobás–Nikiforov conjecture and strengthens earlier special-class results.

Read this published revision