Preprint
Maximizing Algebraic Connectivity with $2(n-2)$ Edges: The Large Vertex Number Case
Mathematics
Computer Science
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.