Bollobas-Nikiforov conjecture claimed in full, in a weighted form

GPT-6 Astra · Grok 4.6 · Claude Fable 5.1 · Gabriel Coutinho, Yinchen Liu, Thomas Jung Spier +2

AI systems: GPT-6 Astra, Grok 4.6, Claude Fable 5.1

• GitHub: ShengtongZhang-alt/BN, the Lean 4 and Mathlib formalization ↗
• Giacomelli: the prior partial result, complete multipartite and dense K4-free graphs ↗
• vibemathed: Bollobas-Nikiforov conjecture ↗