Papers With

← All papers
First page of The positive and negative square-energy conjecture

The positive and negative square-energy conjecture

Yinchen Liu, Quanyu Tang, Shengtong Zhang

math.CO Jul 20, 2026 · v1
formalization combinatorics mathlib
Read PDF arXiv abstract Code
TL;DR
The proof of the main theorem (square-energy conjecture) was formally verified in Lean 4 using Mathlib, with a public GitHub repository.
Abstract
Let $s^+(G)$ and $s^-(G)$ denote the sums of the squares of the positive and negative adjacency eigenvalues of a graph $G$, respectively. We prove the conjecture of Elphick, Farber, Goldberg, and Wocjan that every connected graph $G$ on $n$ vertices satisfies $$ \min\{s^+(G),s^-(G)\}\ge n-1. $$ The proof introduces a new framework for square-energy estimates, in which the Hadamard squares of positive semidefinite matrices that encode these spectral quantities are relaxed to the full doubly nonnegative cone.
Problem

Elphick, Farber, Goldberg, and Wocjan conjectured that every connected graph on n vertices satisfies min{s^+(G), s^-(G)} >= n-1, where s^± are the sums of squares of the positive and negative adjacency eigenvalues.

Approach

The authors prove a doubly nonnegative matrix inequality: 4(sum over edges of sqrt(M_uv))^2 <= (2m-n+1)·1^T M 1. The proof is by induction on vertices, combining folding of non-edge entries, a cut-vertex splitting case, and averaging over vertex deletions. Applying the inequality to the Hadamard squares of the positive and negative spectral parts of A yields the conjecture. The main theorem was formalized in Lean 4 with Mathlib.

Results

The conjecture is proved for all connected graphs, and the disconnected version min{s^+, s^-} >= n-κ(G) follows as a corollary. The proof of the main theorem is machine-checked in Lean.