Bollobás–Nikiforov conjecture

What the AI did

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.

Verification

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.

Sources

• PaperOriginal Bollobás–Nikiforov paper
• Lean proofGitHub repository (Lean 4 proof and preliminary note), pinned to the reviewed commit · Solution.lean: the comparator-checked bridge to the development
• Lean statementChallenge.lean: the five statements against plain Mathlib, at the reviewed commit
• Palomar listingPalomar formalization record
• Problem recordMathDB problem record
• OtherVERIFICATION.md: the recorded comparator and nanoda run