Spectral graph theory & network design
Algebraic Connectivity Maximization
An ongoing research direction combining graph-theory-guided reinforcement learning for network design with exact spectral bounds and formally verified optimality proofs.
- Year
- 2026
- Status
- Ongoing
- Topics
- Graph theory · Reinforcement learning · Spectral methods · Formal verification · Lean
The question
With a fixed number of vertices and edges, how can we build highly connected graphs—and prove when no better graph exists?
Central insight
Finding a strong graph and proving that it is optimal are different tasks. Structural graph families guide the construction algorithms, while spectral arguments establish what any competing graph can achieve.
Graph-Theory-Guided RL for Algebraic Connectivity
A structure-first method for constructing graphs with high algebraic connectivity under strict vertex and edge budgets.
A conceptual illustration of graph construction and spectral connectivity, not a plot of measured experimental results.
The question
With a fixed number of vertices and edges, which network structure coordinates most effectively?
Central insight
The hard part is not only choosing individual edges. Good solutions live near different structural families at different graph densities, so initialization should itself be a mathematical design variable.
Approach
- 01
Route the target density toward complete multipartite or Cayley graph families.
- 02
Construct a low-cost, high-quality structural backbone.
- 03
Use reinforcement learning only for the smaller residual edge-allocation problem.
- 04
Compare quality and runtime against greedy, optimization, and learning baselines.
My contribution
- Developed the density-dependent backbone construction.
- Formulated residual edge allocation as a sequential RL problem.
- Designed and ran the quality-runtime comparison across graph sizes and densities.
A closer look
Why the graph family matters
In continuous-time consensus, each node moves toward its neighbors’ values. The Laplacian describes these interactions, and its second-smallest eigenvalue determines the slowest decaying disagreement mode. A larger value means faster worst-case convergence for this model. The design problem fixes both the number of nodes and the number of edges, so improvement must come from arranging the same resources differently.
The construction begins by choosing a structural family suited to the density. Complete multipartite graphs provide dense backbones; Cayley graphs provide candidates at lower and intermediate densities. This gives the learning stage a useful initial structure and a smaller remaining edge budget.
dx/dt = −Lx, L = D − A
What the policy learns—and what the experiments establish
The policy adds one missing edge at each step until the target budget is exhausted. A graph-attention network scores candidate pairs, and PPO training rewards increases in algebraic connectivity together with a terminal-quality bonus. The learned task is sequential completion of the backbone.
The experiments compare achieved connectivity and runtime against construction baselines, including Fiedler-vector greedy methods. The reported advantage concerns the tested sizes and densities; this method does not establish global optimality for arbitrary vertex and edge budgets. That distinction separates this computational design study from the exact 2(n − 2)-edge theorem within the same research direction.
Result
The backbone-plus-completion strategy achieved the strongest quality/runtime scaling among the tested non-exact baselines as graph size increased.
What remains
Characterize additional near-optimal graph families and make density-aware completion policies lighter and more interpretable.
Maximizing Algebraic Connectivity with 2(n − 2) Edges
A proof of Kolokolnikov’s conjecture: for every n ≥ 4, the maximum is 2, attained by the complete bipartite graph K₂,n−2. The work combines a mathematical proof with a Lean 4 formalization generated using MerLean.
The example is K₂,₆: eight vertices and twelve edges. Assign +1 and −1 to two vertices in the larger part and zero elsewhere. This gives Lx = 2x; the spectrum confirms λ₂ = 2. The theorem shows that no graph with the same budget can exceed it.
The question
How much algebraic connectivity can a graph achieve with exactly 2(n − 2) edges?
Central insight
A hypothetical graph with connectivity above 2 must avoid certain local configurations. Those restrictions force a degree structure in which counting requires a short cycle that the spectral estimates forbid.
Approach
- 01
Use Rayleigh test vectors to turn local graph structure into upper bounds on algebraic connectivity.
- 02
Reduce a counterexample to minimum degree at least three, with no adjacent degree-three vertices.
- 03
Combine degree and incidence counts with an exact non-backtracking Moore bound, and handle the remaining small orders through local cuts.
- 04
Connect the full mathematical argument to the kernel-checked Lean theorem.
My contribution
- Co-first author, with equal contribution alongside Jinzheng Li and Yuanjie Ren.
- Worked on proving the conjecture and formalizing the result in Lean 4 using MerLean.
A closer look
From a candidate graph to a universal bound
Algebraic connectivity is the second-smallest eigenvalue of the graph Laplacian. Computing it for one construction identifies a candidate. Proving optimality requires controlling every simple graph with the same vertex and edge counts. Here K₂,n−2 supplies the candidate: every vertex in one part is connected to every vertex in the other.
|E| = 2(n − 2), n ≥ 4 ⇒ λ₂(G) ≤ 2 = λ₂(K₂,n−2)
Why the contradiction works
The Rayleigh quotient measures the energy of a zero-sum signal on the vertices. Carefully chosen signals certify λ₂ ≤ 2. Assuming the opposite excludes local configurations, leaving a rigid graph whose degree budget can be counted.
For n ≥ 48, an exact Moore bound forces a short cycle that spectral certificates exclude. An incidence argument covers 32 ≤ n ≤ 49; local sparse-set and cut arguments cover 4 ≤ n ≤ 31. The overlapping ranges exhaust all n ≥ 4.
What the formal proof establishes
The released Lean theorem covers every n ≥ 4, rather than a finite numerical search. The repository reports no unfinished proofs and only Lean’s standard axioms. MerLean generated the formal development; Lean checks the resulting proof terms. The accompanying manuscript presents the argument as a conventional mathematical proof.
Result
For all n ≥ 4, every finite simple graph with n vertices and exactly 2(n − 2) edges satisfies λ₂ ≤ 2. The graph K₂,n−2 reaches this bound. Both the upper bound and attainment are included in the formal theorem.
What remains
Classifying all equality cases is a separate problem: the theorem establishes a maximizer, without asserting uniqueness.
Papers & resources
Maximizing Algebraic Connectivity with 2(n − 2) Edges: The Large Vertex Number Case
Zeru Zhu, Jinzheng Li, Yuanjie Ren, and Ji Liu
arXiv:2608.07360 · Revised September 2026 · Preprint
Graph Theory Guided Reinforcement Learning for Network Design with High Algebraic Connectivity under Vertex and Edge Constraints
Zeru Zhu, Marco Gamarra, and Ji Liu
IEEE Conference on Decision and Control (CDC), 2026 · Submitted