Math and TheorySelected results
These are the 11 results I consider the strongest of the 54 in the collection. Each entry states the result and the scope of its formal proof, with links to the manuscript, the Lean proof and the verification steps.
The selection is my own, not an external assessment. The papers have not been externally peer reviewed, and their formal checks apply only to the stated scope.
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.
Formal scope. The theorem for every finite vector of real coefficients, with the exact count of sign vectors and Mathlib's standard normal distribution function, is formalized in 62 Lean modules, including Prawitz smoothing, the characteristic-function envelopes and both analytic zones. Ivanisvili's Theorems 1.1 and 10.9, needed for the full conjecture, are external computer-assisted results and are not formalized.
Manuscript: The small-coefficient upper half of the Keller–Klein conjectureLean proof: The small-coefficient upper half of the Keller–Klein conjectureVerification: The small-coefficient upper half of the Keller–Klein conjecture
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.
Formal scope. The actual-function upper bound and normalized actual-function attainment are formalized, including every horizon and closed parameter boundary. Sharpness for arbitrary L > 0 and radius R > 0 is proved by rescaling in the manuscript, without a separate Lean wrapper.
Manuscript: The exact last-gradient bound for constant-step gradient descent in the strongly convex caseLean proof: The exact last-gradient bound for constant-step gradient descent in the strongly convex caseVerification: The exact last-gradient bound for constant-step gradient descent in the strongly convex case
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
Formal scope. The consensus convergence theorem for 0 < τ ≤ 377359/200000, the arbitrary-rank and full-rank affine-constraint theorems, all seven finite-memory interval certificates and the periodic orbit in R^128 for τ ≥ 1.8868840… are formalized in 301 Lean modules. The scalar theorem, individual objective-value limits, the reduction from proper closed convex functions to proximal attainment, and penalty rescaling are conventional.
Manuscript: A narrow interval for the universal multiplier step of two-block ADMMLean proof: A narrow interval for the universal multiplier step of two-block ADMMVerification: A narrow interval for the universal multiplier step of two-block ADMM
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.
Formal scope. The strict separation at every adjacent level, for the actual semidefinite programs with unrestricted complex auxiliaries and positive-definite trace-one states with positive Bell coefficients, and the absence of a universal finite collapse are formalized in 17 Lean modules. The operational exact-cost and tensor-multiplicativity consequences use published theorems of Lami, Mele and Regula.
Manuscript: No universal finite collapse of the upper PPT entanglement-cost hierarchyLean proof: No universal finite collapse of the upper PPT entanglement-cost hierarchyVerification: No universal finite collapse of the upper PPT entanglement-cost hierarchy
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.
Formal scope. Both implications are formalized in two Lean projects. The Lean 4.35 project states the conjecture for every finite Artin–Schreier tower over a base whose valuation ring is henselian in Mathlib's sense, with depth one defined as the least length of a complete Mac Lane–Vaquié chain over all primitive generators; it compares these chains with Okutsu sequences at length one only. The Lean 4.19 project states depth one through Okutsu sequences in the algebraic closure of K inside the Hahn field.
Manuscript: Depth-one Artin–Schreier defect towers are compositaLean proof: Depth-one Artin–Schreier defect towers are compositaVerification: Depth-one Artin–Schreier defect towers are composita
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.
Formal scope. The explicit equivalence over every infinite field, for arbitrary rectangular pencils, every border size and distinct anchors including eigenvalues, and the common-summand cancellation are formalized in two Lean projects. The identification with the barred pencils of the conjecture uses a published linearization theorem and is not formalized.
Manuscript: Matrix-pencil rank distance as an explicit completion problemLean proof: Matrix-pencil rank distance as an explicit completion problemVerification: Matrix-pencil rank distance as an explicit completion problem
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).
Formal scope. The whole family is formalized in Lean, with nonnegative rank minimized over all real nonnegative factorizations, together with a literal negation of the conjecture over all finite rectangular nonnegative real matrices. The width-109 factorization of the order-11 witness is also checked in exact rational arithmetic. The exact nonnegative rank of the squares is not determined.
Manuscript: Counterexamples to the Kronecker-square lower bound for nonnegative rankLean proof: Counterexamples to the Kronecker-square lower bound for nonnegative rankVerification: Counterexamples to the Kronecker-square lower bound for nonnegative rank
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.
Formal scope. Lean 4.19.0 proves, for the inversion-weighted q-permanent of ordered real matrices, the endpoint identity 2D₁(VVᵀ) = C(n,2)‖f‖² − ‖G‖² for every real n × 3 matrix, soundness of the four-row integer certificate for every type list, the reduction of a negative endpoint to a rational positive-definite matrix with rational 0 < q₁ < q₂ < 1, identity padding, rank three of the frozen witness and the all-orders statement from its certificate inequality; a strict audit covers all 749 project declarations other than code-generation auxiliaries, with no native evaluation. The finite comparison for the 896-row witness is checked outside Lean by two independent exact programs, one of which determines per(B) and the wedge norms through the Chinese remainder theorem. The explicit regularization and the asymptotic and spectral theorems are conventional.
Manuscript: Finite real counterexamples and spectral obstructions for q-permanent monotonicityLean proof: Finite real counterexamples and spectral obstructions for q-permanent monotonicityVerification: Finite real counterexamples and spectral obstructions for q-permanent monotonicity
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.
Formal scope. The formal proof includes arbitrary dimensions, the exact moment identities, the Hamming-distance bound, and sharpness witnesses.
Manuscript: The sharp level-one Fourier weight at density one eighthLean proof: The sharp level-one Fourier weight at density one eighthVerification: The sharp level-one Fourier weight at density one eighth
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.
Formal scope. The continuous-time Hilbert-space threshold, the discrete threshold and the planar escape for 1 < r ≤ 2, including actual gradients, global solutions from rest and norm divergence, are formalized. The planar escape of the same potential for 0 < r ≤ 1, its boundedness for r > 2 and existence of solutions for r ≤ 1 are conventional.
Manuscript: Escaping Nesterov flows and iterates below critical dampingLean proof: Escaping Nesterov flows and iterates below critical dampingVerification: Escaping Nesterov flows and iterates below critical damping
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.
Formal scope. The proof constructs local basis permutations and establishes their finite complex Hilbert-space interpretation. Arbitrary changes to an external Schmidt basis are not separately formalized.
Manuscript: Universal entanglement embezzlement with inverse-quadratic logarithmic infidelityLean proof: Universal entanglement embezzlement with inverse-quadratic logarithmic infidelityVerification: Universal entanglement embezzlement with inverse-quadratic logarithmic infidelity