Papers With

← All papers
First page of Maximizing Algebraic Connectivity with $2(n-2)$ Edges: The Large Vertex Number Case

Maximizing Algebraic Connectivity with $2(n-2)$ Edges: The Large Vertex Number Case

Zeru Zhu, Jinzheng Li, Yuanjie Ren, Ji Liu

math.CO Aug 7, 2026 · v2 cs.LO math.SP
formalization combinatorics ai-agents
Read PDF arXiv abstract Code
TL;DR
A Lean 4 formalization of Kolokolnikov's conjecture for all n≥4 was generated with MerLean and checked by the Lean kernel, with a public repository.
Abstract
Kolokolnikov conjectured that, among all simple graphs on \(n\) vertices with exactly \(2(n-2)\) edges, the complete bipartite graph maximizes algebraic connectivity. This paper proves the conjecture. The underlying Lean 4 formalization was generated with MerLean and checked by the Lean kernel.
Problem

Kolokolnikov conjectured that among simple graphs on n vertices with exactly 2(n-2) edges, the complete bipartite graph K_{2,n-2} maximizes algebraic connectivity, i.e. λ2(G) ≤ 2.

Approach

The proof argues by contradiction. Rayleigh-quotient certificates exclude low-degree vertices and certain local configurations, which reduces a counterexample to a degree-3-separated obstruction. Global degree counting gives a master inequality. A Moore-type breadth-first-search bound forces a short cycle, while spectral certificates forbid such cycles, and an arithmetic overlap lemma shows the two conflict. The full conjecture was also formalized in Lean 4 using MerLean.

Results

The human-readable proof establishes λ2(G) ≤ 2 for all n ≥ 123, so K_{2,n-2} is a maximizer in that range. The Lean formalization, checked by the Lean kernel, covers every n ≥ 4.