Bollobas-Nikiforov conjecture claimed in full, in a weighted form
Five named mathematicians with AI assistance claim the 2007 Bollobas-Nikiforov conjecture for every noncomplete graph, bounding the sum of the squares of the two largest adjacency eigenvalues, with a Lean formalization.
- Lab
- Independent
- Model
- GPT-6 Astra (ideation and manuscript); Grok 4.6 (Lean formalization); Claude Fable 5.1 (submission packaging)
- Field
- Mathematics
- Date
- 2026-09-06
- Human collaborators
- Gabriel Coutinho, Yinchen Liu, Thomas Jung Spier, Quanyu Tang, Shengtong Zhang
- Problem posed
- 2007 · open 19 yrs
What was found
Bollobas and Nikiforov conjectured in 2007 that every noncomplete graph on at least two vertices satisfies a bound on the sum of the squares of its two largest adjacency eigenvalues, in terms of its edge count and clique number. The repository formalizes the conjecture together with a weighted spectral inequality and a completely positive matrix theorem that prove it, and carries a Palomar registration. The AI roles are split and disclosed individually: ideation and the manuscript from GPT-6 Astra, the Lean development completed by Grok 4.6 with minimal direction, and submission packaging by a Claude agent.
Novelty check
The conjecture dates to 2007. The strongest previously published result found is Giacomelli (arXiv:2603.26379), a single-author paper with no AI disclosure, which proves the conjecture only for complete multipartite graphs and for dense K4-free graphs. This claim is materially larger: the general conjecture for every noncomplete graph, in a stronger weighted form, submitted some months later. The gap between the two is the reason to record this early and to state plainly that it has not been checked.
Caveats and known objections
The jump from the published partial results to a claimed full resolution is the thing to verify first, and nobody outside the five authors has done it. The grade is claimed rather than formal because the Palomar record establishes that the Lean typechecks against the recorded statement, not that the recorded statement is the conjecture in its general form. Autonomy is collaborative rather than ai-led: the disclosure describes ideation as human and model back and forth among five named mathematicians rather than a model producing the argument, and the formalization step was a separate model working from an already written proof.
Machine-checked elsewhere
PalomarPALOMAR-2026-09-07-000002
ShengtongZhang-alt/BN
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Also recorded at
vibemathedbollobas-nikiforov-conjecture
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Bollobas-Nikiforov conjecture claimed in full, in a weighted form. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-06-bollobas-nikiforovBibTeX
@misc{whataifound-independent-2026-nikiforov,
title = {Bollobas-Nikiforov conjecture claimed in full, in a weighted form},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Claimed. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-09-06-bollobas-nikiforov}
}