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

Ji Liu; Jinzheng Li; Yuanjie Ren; Zeru Zhu

REVIEW 1 major objections 4 minor 12 references

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

T0 review · 1 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read For $n\ge123$, every graph with $2(n-2)$ edges has algebraic connectivity at most $2$; the complete bipartite graph $K_{2,n-2}$ attains this maximum.

desk verdict Solid large-n resolution of Kolokolnikov's conjecture with one unexpanded polynomial identity and a Lean claim that needs independent audit; deserves review. read the letter →

arxiv 2608.07360 v1 pith:CN3LYNED submitted 2026-08-07 math.CO cs.LOmath.SP

Zeru Zhu , Jinzheng Li , Yuanjie Ren , Ji Liu This is my paper · ORCID

classification math.COcs.LOmath.SP MSC 05C5005C3505C3868V1568V20

keywords algebraicconnectivityLaplacianeigenvalueextremalgraphtheorycompletebipartiteMooreboundRayleighquotientcertificatedegreecountingmachine-checkedproof

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper proves a conjectured extremal bound for a standard measure of graph connectivity, the second-smallest Laplacian eigenvalue $\lambda_2$. The result: for every $n\ge123$, any finite simple graph with $n$ vertices and exactly $2(n-2)$ edges has $\lambda_2(G)\le2$. The complete bipartite graph $K_{2,n-2}$, which connects two vertices to all of the other $n-2$, has exactly this many edges and attains $\lambda_2=2$, so it is a maximizer in this range. The proof rules out a hypothetical counterexample by combining explicit Rayleigh-quotient certificates, a global degree count, and a Moore-type short-cycle argument whose two criteria are shown to overlap for $n\ge123$. The paper also reports a machine-checked formalization of the full conjecture for every $n\ge4$.

What carries the argument

Three interacting mechanisms carry the proof. (1) Rayleigh-quotient certificates: if a nonzero vector $x$ with coordinate sum zero has Dirichlet energy at most twice its squared norm, then $\lambda_2(G)\le2$; the paper constructs such vectors to exclude low-degree vertices, adjacent degree-$3$ vertices, and several local neighborhood patterns, reducing any counterexample to a degree-$3$-separated obstruction in which degree-$3$ vertices form an independent set. (2) Global degree count: double-counting edges out of the degree-$3$ set yields the master inequality $10X+7h\le4n-200$ and the edge-excess bound $e(S)\ge|S|+t$ with $t=n-4-X-3h$. (3) Paired cycle criteria: a Moore-type breadth-first-search double count shows that enough edge excess forces a cycle of length at most $2r+1$, and a spectral certificate excludes every cycle of that length; the arithmetic identity (5.6) in Lemma 5.1 is what makes the two ranges overlap.

What would settle it

Mechanically expand both sides of identity (5.6) in the polynomial ring and compare; if the identity fails for any $n\ge123$, the overlap argument collapses and the proof must be repaired. Alternatively, search computationally for a graph with $n\ge123$ vertices, exactly $2(n-2)$ edges, and $\lambda_2>2$; any such graph would be a direct counterexample to Theorem 1.2.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that the extremal conjecture for algebraic connectivity is true at all sufficiently large orders: any graph with $n\ge123$ vertices and exactly $2n-4$ edges must satisfy $\lambda_2(G)\le2$, and the complete bipartite graph $K_{2,n-2}$ attains $\lambda_2=2$. Assuming $\lambda_2(G)>2$ for a hypothetical counterexample, local spectral certificates force the degree-$3$ vertices to form an independent set and bound how many degree-$3$ neighbors any vertex can absorb. A global degree count then reduces the high-degree structure to two parameters, the number $h$ of vertices of degree at least $5$ and their total excess $X$ over degree $4$, constrained by $10X+7h\le4n-200$. The low-degree induced subgraph $S$ is shown to have enough edge excess to force a short cycle, while a spectral low-degree cycle certificate forbids cycles in the same length range. Lemma 5.1 shows these two opposing criteria overlap for $n\ge123$, yielding the contradiction.

Load-bearing premise

The load-bearing premise is that the algebraic expansion leading to identity (5.6) is exactly correct, since the contradiction depends on that identity and on the positivity of the three polynomials it defines for $n\ge123$.

Editorial extensions

If this is right

For every $n\ge123$, the maximum algebraic connectivity among $n$-vertex simple graphs with exactly $2(n-2)$ edges is exactly $2$, attained by $K_{2,n-2}$.
The extremal problem is closed for all sufficiently large orders: no graph in this class can have $\lambda_2$ above $2$.
Equality cases are left unclassified; the paper proves maximality, not uniqueness of the maximizer.
The reported machine-checked formalization covers every $n\ge4$, so if that formalization is trustworthy the conjecture is known for all $n\ge4$, not only $n\ge123$.
A reusable proof pattern is established: pin down local structure with spectral certificates, constrain the global degree sequence, then let edge excess force a short cycle that a spectral bound forbids.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The threshold $123$ comes from an explicit positivity check of three polynomials and is almost certainly not the true turning point; the same proof scheme may extend to lower $n$ by sharper estimates, potentially covering every order with a single human-readable argument.
The rigid degree-$3$-separated obstruction structure may make equality cases tractable: one could search inside this class for graphs with $\lambda_2=2$, revealing whether $K_{2,n-2}$ is unique or part of a larger family.
The paired cycle criteria, in which positive edge excess forces a short cycle while a spectral bound forbids it, look transferable to other extremal spectral problems with fixed order and size once local structure is constrained by certificates.
A human-readable proof for $4\le n\le122$ would let mathematicians verify the full conjecture without relying on the reported machine-checked formalization; until then the small-order range rests on the correctness of that formalization.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The main theorem is real and the proof is in good shape. The authors prove that for every n≥123, any simple graph on n vertices with 2(n−2) edges has algebraic connectivity at most 2, with K_{2,n−2} attaining equality. That is a genuine advance on Kolokolnikov's conjecture. I traced the local Rayleigh certificates (Lemmas 2.3–2.9), the degree-capacity inequalities (Lemmas 3.1–3.6), the paired cycle criteria (Propositions 4.2–4.3), and the arithmetic overlap (Lemma 5.1, Proposition 5.2). The logic is coherent, the certificates directly construct Rayleigh vectors, and the degree counts are honest. No fitted parameters, no circularity. The combination of explicit spectral certificates with an irregular Moore bound and a two-variable degree count is a new, reusable technique. The proof is self-contained for the n≥123 range, and the paper says so.

The soft spots are two, and both are minor but worth naming. First, Lemma 5.1's identity (5.6) is asserted by "a direct expansion gives" and is genuinely load-bearing: the threshold n≥123 and the strict inequality (5.5) depend on it. The identity is checkable by hand or by a few lines of computer algebra, and my own spot-checking makes me confident it is correct. Still, a referee should ask the authors to display the expansion or provide a small script. It is an omitted computational verification, not a conceptual gap. Second, the appendix's claim that the full conjecture for all n≥4 is Lean-kernel-checked is remarkable, but the paper gives no commit hash and no independent audit of the formalization. The link to the repository exists, and the comparator tool is mentioned, but the paper itself cannot be verified from the PDF alone. The human-readable proof of the complementary range 4≤n≤122 is explicitly deferred, so as a reader I can only rely on the n≥123 part. That limitation is transparently stated in Section 6, and it does not weaken the main theorem.

One more observation: the appendix spends considerable space describing the MerLean agent, token counts, and system architecture. This is self-promotional and not needed for the mathematics. It is harmless but distracts from the actual result. The citation pattern is fine—the MerLean papers are cited because they are the tool, and the self-citation is not hiding anything.

Who is this for? Spectral graph theorists and people working on extremal Laplacian problems. The paper deserves a serious referee. The unexpanded identity and the Lean claim should be addressed, but the core theorem holds up and is worth publishing.

Referee Report

1 major / 4 minor

Summary. The paper proves Kolokolnikov's conjecture for all n ≥ 123: every finite simple graph on n vertices with exactly 2(n−2) edges has algebraic connectivity at most 2, and since K_{2,n−2} attains value 2, it is a maximizer. The proof is by contradiction. It first uses explicit Rayleigh-quotient test vectors to exclude vertices of degree ≤ 2 and adjacent degree-3 vertices, which forces a hypothetical counterexample into a rigid 'degree-3-separated obstruction' class. A global degree count then yields a master inequality involving the number h of high-degree vertices and the excess X of their degrees above 4, together with an edge-excess bound for the subgraph induced by low-degree vertices. Two opposing criteria are derived for that subgraph: a Moore-type breadth-first-search bound that forces a short cycle when the edge excess is large, and a spectral certificate that forbids cycles in the same length range. The paper closes by proving, in Lemma 5.1, that the two criteria overlap once n ≥ 123. An appendix claims that Conjecture 1.1 has been fully formalized and kernel-checked in Lean for all n ≥ 4.

Significance. If Theorem 1.2 is correct, it resolves the asymptotic form of Kolokolnikov's conjecture with an explicit threshold, giving a clean extremal result for algebraic connectivity under a natural edge budget. The proof strategy is elementary and modular: variational Rayleigh certificates, degree-capacity counting, a Moore-type double count, and a final arithmetic overlap. This may generalize to other extremal spectral problems. The paper also claims a machine-checked Lean formalization of the full conjecture for all n ≥ 4; if the associated artifact is publicly auditable, that is a substantial verification milestone. However, the human-readable part of the proof stands on its own, and the formalization appendix is not needed for Theorem 1.2. The main value of the paper is the self-contained proof for large n, which is presented in a clear and organized way.

major comments (1)

[§5.1, Eq. (5.6)] The proof of Lemma 5.1, and hence the entire overlap argument for n ≥ 123, depends on the polynomial identity 4913γ − 1000φ3(n) = 289(m−17h)φ2(n) + 17(m²−(17h)²)φ1(n) + 25921(m³−(17h)³). This identity is asserted with the phrase 'A direct expansion gives' and is not derived, displayed, or otherwise verified in the text. Since the strict inequality (5.5) and the threshold n ≥ 123 rest on the positivity of the right-hand side, I request that the authors provide the expanded identity, supply a machine-checkable certificate (e.g., a small computer algebra transcript), or cite the specific lemma in the accompanying Lean development that discharges this calculation. Without such support, the central numerical step is not independently verifiable from the paper.

minor comments (4)

[Appendix A] The formalization claim would be reproducible if the paper included the commit hash of the GitHub repository github.com/MerLeanProver/ACMaxConjecture and the exact Lean version and mathlib version used for the kernel check.
[Throughout] There are minor typographical issues, including the missing spaces in the title/abstract ('with2(n−2)Edges') and the inconsistent notation 'D3' versus 'D_3' near Definition 2.10.
[Appendix A] The statement 'Every numerical certificate was cross-checked by exact big-integer enumeration before formalization' is vague; please clarify which certificates are meant, since the main proof appears to contain only the single identity (5.6) as a numerical/algebraic check.
[Section 4.2] In Proposition 4.3, the condition (4.7) is justified by Lemma 2.9, but the proof would be easier to follow if the role of the term '12' in '24r + X + 12' were explicitly matched to the length bound 2r + 1.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Theorem 1.2 is proved from explicit Rayleigh certificates, degree counting, and an arithmetic overlap; the Lean/MerLean material is tooling support and does not substitute for the human proof.

full rationale

The derivation is self-contained. Theorem 1.2 is proved by contradiction using explicit Rayleigh-quotient certificates (Proposition 2.2, Lemmas 2.3–2.9), global degree constraints (Lemma 3.3, Corollary 3.5, Lemma 3.6), paired cycle criteria (Lemma 4.1, Propositions 4.2 and 4.3), and a quantitative overlap (Lemma 5.1). No parameter is fitted to force the conclusion: every spectral certificate directly constructs a Rayleigh vector satisfying the Courant–Fischer bound, and the arithmetic overlap is proved from the stated inequalities h≤X and 10X+7h≤4n−200 together with positivity of explicit polynomials for n≥123. The unexpanded identity (5.6) is an algebraic expansion that is displayed; even if it were wrong, that would be a correctness defect, not circularity, because it does not define the target quantity in terms of itself. The MerLean self-citations [7,10] concern the formalization toolchain, not the mathematical derivation; Appendix A additionally reports a Lean kernel check with an axiom whitelist and an external comparator audit. The human-readable proof of Theorem 1.2 does not rely on those self-citations for its validity. Hence there is no circular step that reduces the conclusion to its inputs.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The proof relies only on standard spectral graph theory (Courant-Fischer min-max, Fiedler's Laplacian eigenvalue definition), the degree-sum identity, and the paper's own structural lemmas. The threshold n=123 is derived, not fitted; no free parameters or invented entities are introduced. The claimed Lean formalization is external support, not an axiom of the paper's mathematical argument.

assumptions (3)

standard math Courant-Fischer variational characterization of λ2 as the minimum Rayleigh quotient over zero-sum vectors
Used in Section 2.1, equation (2.1), as the starting point of every Rayleigh certificate.
standard math Algebraic connectivity is the second smallest Laplacian eigenvalue, following Fiedler's definition
Foundational definition of λ2 used throughout; cited to Fiedler [4].
standard math Degree-sum identity Σ d(v)=2|E| and the derived relation Σ(d(v)-3)=n-8 under minimum degree at least 3
Used in Lemmas 2.4, 2.6-2.9, 3.1, 3.6, and the cycle certificates.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Maximizing Algebraic Connectivity with $2(n-2)$ Edges: The Large Vertex Number Case." pith.science (2026). https://pith.science/paper/CN3LYNED

@misc{pith2026260807360,
  author       = {Pith},
  title        = {Pith review of: Maximizing Algebraic Connectivity with $2(n-2)$ Edges: The Large Vertex Number Case},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CN3LYNED}},
  note         = {Machine review of arXiv:2608.07360}
}

abstract

Kolokolnikov conjectured that, among finite simple graphs on $n$ vertices with exactly $2(n-2)$ edges, the complete bipartite graph $K_{2,n-2}$ maximizes algebraic connectivity. We prove the conjectured statement for every $n\ge123$: every such graph has algebraic connectivity at most $2$, while $K_{2,n-2}$ attains $2$. The proof begins with explicit Rayleigh-quotient certificates that exclude several local configurations from a hypothetical counterexample. A global degree count then controls the number and total excess of vertices of degree at least $5$ and bounds the edge excess of the subgraph induced by vertices of degree at most $4$. A Moore-type breadth-first-search criterion uses this excess to guarantee a short cycle, while a spectral criterion excludes cycles in the same length range. An explicit arithmetic estimate shows that the two criteria apply simultaneously once $n\ge123$. A Lean formalization covering every $n\ge4$, including the complementary range $4\le n\le122$, has been produced with MerLean and checked by the Lean kernel; the present paper gives a self-contained mathematical account of the large-order component.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

12 extracted references · 5 canonical work pages

[1]

The Moore bound for irregular graphs

N. Alon, S. Hoory, and N. Linial. “The Moore bound for irregular graphs”. In:Graphs and Combinatorics18 (2002), pp. 53–57.doi:10.1007/s003730200002

doi:10.1007/s003730200002 2002
[2]

A. E. Brouwer and W. H. Haemers.Spectra of Graphs. Universitext. New York: Springer, 2012.doi:10.1007/978-1-4614-1939-6

doi:10.1007/978-1-4614-1939-6 2012
[3]

Chhikara, D

P. Chhikara, D. Khant, S. Aryan, T. Singh, and D. Yadav.Mem0: Building Production-Ready AI Agents with Scalable Long-Term Memory. 2025. arXiv:2504.19413 [cs.CL]

arXiv 2025
[4]

Algebraic connectivity of graphs

M. Fiedler. “Algebraic connectivity of graphs”. In:Czechoslovak Mathematical Journal23 (1973), pp. 298–305.doi:10.21136/CMJ.1973.101168

work page arXiv 1973
[5]

G. Gao, H. Ju, J. Jiang, Z. Qin, and B. Dong.A Semantic Search Engine for Mathlib4. 2025. arXiv:2403 . 13310 [cs.IR]. Published inFindings of the Association for Computational Linguistics: EMNLP 2024, Association for Computational Linguistics, pp. 8001–8013,https: //doi.org/10.18653/v1/2024.findings-emnlp.470

doi:10.18653/v1/2024.findings-emnlp.470 2025
[6]

Maximizing algebraic connectivity for certain families of graphs

T. Kolokolnikov.Maximizing algebraic connectivity for certain families of graphs. 2014. arXiv: 1412.6147 [cs.DM]. Published inLinear Algebra and its Applications471(2015), 122–140, https://doi.org/10.1016/j.laa.2014.12.023

work page Pith review arXiv 2015
[7]

J. Li, Z. Zhu, and Y. Ren.MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving. 2026. arXiv:2605.26959 [cs.LO]

work page Pith review arXiv 2026
[8]

The Lean 4 theorem prover and programming language

L. de Moura and S. Ullrich. “The Lean 4 theorem prover and programming language”. In: Automated Deduction – CADE 28. Vol. 12699. Lecture Notes in Computer Science. Cham: Springer, 2021, pp. 625–635.doi:10.1007/978-3-030-79876-5_37

doi:10.1007/978-3-030-79876-5_37 2021

Show all 12 references

[9]

Maximizing Algebraic Connectivity in the Space of Graphs with a Fixed Number of Vertices and Edges

K. Ogiwara, T. Fukami, and N. Takahashi. “Maximizing Algebraic Connectivity in the Space of Graphs with a Fixed Number of Vertices and Edges”. In:IEEE Transactions on Control of Network Systems4.2 (2017), pp. 359–368.doi:10.1109/TCNS.2015.2503561

2017
[10]

Y. Ren, J. Li, and Y. Qi.MerLean: An Agentic Framework for Autoformalization in Quantum Computation. 2026. arXiv:2602.16554 [cs.LO]

2026
[11]

Algebraic Connectivity: Local and Global Max- imizer Graphs

K. Shahbaz, M. N. Belur, and A. Ganesh. “Algebraic Connectivity: Local and Global Max- imizer Graphs”. In:IEEE Transactions on Network Science and Engineering10.3 (2023), pp. 1636–1647.doi:10.1109/TNSE.2022.3232397. 14

2023
[12]

2019.doi:10

The mathlib Community.The Lean mathematical library. 2019.doi:10 . 1145 / 3372885 . 3373824. arXiv:1910.09336 [cs.LO]. A Formalization and AI agent design Conjecture 1.1 has been formalized and proved in full generality (for everyn≥4, not only the large- order range treated he...

2019 arXiv

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [1]

The Moore bound for irregular graphs

N. Alon, S. Hoory, and N. Linial. “The Moore bound for irregular graphs”. In:Graphs and Combinatorics18 (2002), pp. 53–57.doi:10.1007/s003730200002

doi:10.1007/s003730200002 2002

[2] [2]

A. E. Brouwer and W. H. Haemers.Spectra of Graphs. Universitext. New York: Springer, 2012.doi:10.1007/978-1-4614-1939-6

doi:10.1007/978-1-4614-1939-6 2012

[3] [3]

Chhikara, D

P. Chhikara, D. Khant, S. Aryan, T. Singh, and D. Yadav.Mem0: Building Production-Ready AI Agents with Scalable Long-Term Memory. 2025. arXiv:2504.19413 [cs.CL]

arXiv 2025

[4] [4]

Algebraic connectivity of graphs

M. Fiedler. “Algebraic connectivity of graphs”. In:Czechoslovak Mathematical Journal23 (1973), pp. 298–305.doi:10.21136/CMJ.1973.101168

work page arXiv 1973

[5] [5]

G. Gao, H. Ju, J. Jiang, Z. Qin, and B. Dong.A Semantic Search Engine for Mathlib4. 2025. arXiv:2403 . 13310 [cs.IR]. Published inFindings of the Association for Computational Linguistics: EMNLP 2024, Association for Computational Linguistics, pp. 8001–8013,https: //doi.org/10.18653/v1/2024.findings-emnlp.470

doi:10.18653/v1/2024.findings-emnlp.470 2025

[6] [6]

Maximizing algebraic connectivity for certain families of graphs

T. Kolokolnikov.Maximizing algebraic connectivity for certain families of graphs. 2014. arXiv: 1412.6147 [cs.DM]. Published inLinear Algebra and its Applications471(2015), 122–140, https://doi.org/10.1016/j.laa.2014.12.023

work page Pith review arXiv 2015

[7] [7]

J. Li, Z. Zhu, and Y. Ren.MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving. 2026. arXiv:2605.26959 [cs.LO]

work page Pith review arXiv 2026

[8] [8]

The Lean 4 theorem prover and programming language

L. de Moura and S. Ullrich. “The Lean 4 theorem prover and programming language”. In: Automated Deduction – CADE 28. Vol. 12699. Lecture Notes in Computer Science. Cham: Springer, 2021, pp. 625–635.doi:10.1007/978-3-030-79876-5_37

doi:10.1007/978-3-030-79876-5_37 2021