Math and Theory

Selected results

The 11 results I consider the strongest; my own selection, not an external assessment. The same results with their formal scope.

1. The small-coefficient upper half of the Keller–Klein conjecture

   Partially resolvedKeller–Klein conjecture on Berry–Esseen bounds for Rademacher sums

   For X = Σ vᵢεᵢ with independent uniform signs, Σ vᵢ² = 1 and |vᵢ| ≤ a ≤ 7/100, P(X ≤ x) − Φ(x) ≤ Φ(a) − 1/2 for every x ≥ 0: the upper half of the Keller–Klein conjecture in this small-coefficient range.

   Manuscript: The small-coefficient upper half of the Keller–Klein conjecture · Lean proof: The small-coefficient upper half of the Keller–Klein conjecture · Verification: The small-coefficient upper half of the Keller–Klein conjecture

2. The exact last-gradient bound for constant-step gradient descent in the strongly convex case

   ProvedTaylor–Hendrickx–Glineur Conjecture 3: last-iterate gradient norm of gradient descent

   Gradient descent with step h/L, 0 ≤ h ≤ 2, on L-smooth μ-strongly convex f on any real Hilbert space satisfies ‖∇f(x_N)‖ ≤ L‖x₀ − x*‖ max{p_N(μ/L, h), |1 − h|^N} for every N, with equality attained in one dimension.

   Manuscript: The exact last-gradient bound for constant-step gradient descent in the strongly convex case · Lean proof: The exact last-gradient bound for constant-step gradient descent in the strongly convex case · Verification: The exact last-gradient bound for constant-step gradient descent in the strongly convex case

3. A narrow interval for the universal multiplier step of two-block ADMM

   Partially resolvedGlowinski's open question on the ADMM dual step size beyond the golden ratio

   Two-block ADMM with multiplier step τ converges for every 0 < τ ≤ 1.886795 on finite-dimensional convex problems with attained proximal steps and a saddle point; fixed polytopes in R^128 cycle for every τ ≥ 1.8868840…; scalar problems converge exactly for 0 < τ < 2

   Manuscript: A narrow interval for the universal multiplier step of two-block ADMM · Lean proof: A narrow interval for the universal multiplier step of two-block ADMM · Verification: A narrow interval for the universal multiplier step of two-block ADMM

4. No universal finite collapse of the upper PPT entanglement-cost hierarchy

   Answered negativelyFinite collapse of the Lami–Mele–Regula upper PPT entanglement-cost hierarchy

   For every q ≥ 1 a full-rank product-Bell-diagonal state in local dimension 2^((2q+4)4^q) has κ_{q+1}(ρ) < κ_q(ρ), so no fixed finite level of the upper PPT entanglement-cost hierarchy is exact for all states.

   Manuscript: No universal finite collapse of the upper PPT entanglement-cost hierarchy · Lean proof: No universal finite collapse of the upper PPT entanglement-cost hierarchy · Verification: No universal finite collapse of the upper PPT entanglement-cost hierarchy

5. Depth-one Artin–Schreier defect towers are composita

   ProvedNart–Novacoski conjecture on depth-one Artin–Schreier defect towers

   Over a perfect henselian K ⊆ k((y^ℚ)) containing k(y) without finite accumulation points (k algebraically closed, char. p), each nontrivial finite Artin–Schreier tower of depth one is a compositum of Artin–Schreier extensions.

   Manuscript: Depth-one Artin–Schreier defect towers are composita · Lean proof: Depth-one Artin–Schreier defect towers are composita · Verification: Depth-one Artin–Schreier defect towers are composita

6. Matrix-pencil rank distance as an explicit completion problem

   ProvedDodig–Stošić conjecture on bounded rank perturbations of matrix pencils

   Over any infinite field, pencils A, B have δ(A,B) ≤ x exactly when K_{c,d}(A) is a constant full-rank compression of K_{c,d}(B) ⊕ (t − d)I_x; a cited linearization theorem then gives Conjecture 1 over algebraically closed fields.

   Manuscript: Matrix-pencil rank distance as an explicit completion problem · Lean proof: Matrix-pencil rank distance as an explicit completion problem · Verification: Matrix-pencil rank distance as an explicit completion problem

7. Counterexamples to the Kronecker-square lower bound for nonnegative rank

   DisprovedVandaele–Gillis–Glineur–Tuyttens conjecture rank₊(M ⊗ M) ≥ rank₊(M) rank(M)

   For every k ≥ 0 an explicit rational nonnegative matrix C of order k + 11, rank k + 10 and nonnegative rank k + 11 has rank₊(C ⊗ C) ≤ (k + 10)² + 9, at least k + 1 below the conjectured bound rank₊(C) rank(C).

   Manuscript: Counterexamples to the Kronecker-square lower bound for nonnegative rank · Lean proof: Counterexamples to the Kronecker-square lower bound for nonnegative rank · Verification: Counterexamples to the Kronecker-square lower bound for nonnegative rank

8. Finite real counterexamples and spectral obstructions for q-permanent monotonicity

   Disproved for real symmetric positive-definite matricesReal-symmetric case of the Bapat–Lal q-permanent monotonicity conjecture on [−1,1]

   An explicit integer positive-definite matrix of order 896 has a q-permanent that strictly decreases between two explicit rationals in (0,1); counterexamples exist in every order N ≥ 896.

   Manuscript: Finite real counterexamples and spectral obstructions for q-permanent monotonicity · Lean proof: Finite real counterexamples and spectral obstructions for q-permanent monotonicity · Verification: Finite real counterexamples and spectral obstructions for q-permanent monotonicity

9. The sharp level-one Fourier weight at density one eighth

   Determined exactlyLei Yu's problem on the level-1 Fourier weight W(1/8) of Boolean functions of density 1/8

   Every Boolean function of mean 1/8 on {−1,1}^n has level-one Fourier weight at most 3/64, attained by a codimension-three subcube for n ≥ 3; equivalently, density-1/8 sets have average Hamming distance ≥ (n − 3)/2.

   Manuscript: The sharp level-one Fourier weight at density one eighth · Lean proof: The sharp level-one Fourier weight at density one eighth · Verification: The sharp level-one Fourier weight at density one eighth

10. Escaping Nesterov flows and iterates below critical damping

    Partially resolvedBoundedness of Nesterov ODE trajectories and iterates below critical damping r < 3

    On ℓ²(ℕ;ℝ²), Nesterov flows from rest and iterates with momentum k/(k+r) stay bounded for all convex objectives with 1-Lipschitz gradient and attained minimum exactly when r ≥ 3; a planar potential escapes for 0 < r ≤ 2.

    Manuscript: Escaping Nesterov flows and iterates below critical damping · Lean proof: Escaping Nesterov flows and iterates below critical damping · Verification: Escaping Nesterov flows and iterates below critical damping

11. Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity

    Answered positivelyLeung–Wang question on the rate of general universal entanglement embezzling families

    For each L ≥ 1 one target-independent catalyst of local dimension n = 2^(4L) lets local basis permutations reach root fidelity at least 1 − 125m/L² = 1 − 2000m/(log₂ n)² for every Schmidt probability vector on m entries.

    Manuscript: Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity · Lean proof: Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity · Verification: Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity

Index of results

All 54 manuscripts, by discipline and subject. Every result has its own page with the theorem, what Lean checks and what rests on a conventional proof, the manuscript and its LaTeX source, the Lean files, and the commands for reproducing the checks. Problems and conjectures names the problem each result addresses and its status, and Subjects gives an overview of the subjects.

No results match. Try fewer or shorter words, or clear the filters.

Models used

• GPT 6 Astra by OpenAI, in ChatGPT and Codex
• GPT 6.1 Sol by OpenAI, in Codex
• Opus 5.5 by Anthropic, in Claude Code

Each manuscript states how these models were used for it.