Math and TheoryThe small-coefficient upper half of the Keller–Klein conjecture
Selected result in this collection
Problem and result
- Problem
- Keller–Klein conjecture on Berry–Esseen bounds for Rademacher sums
- Posed in
- Keller and Klein, Advances in Mathematics 407 (2022), 108558, Conjecture 9.3 (in their proof of Tomaszewski's conjecture)
- Status
- Partially resolved
- Result
- 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.
Abstract
Let X = Σ vᵢεᵢ with independent uniform signs, real coefficients, Σ vᵢ² = 1 and |vᵢ| ≤ a, where 0 < a ≤ 7/100. For every x ≥ 0, P(|X| ≤ x) ≤ 2Φ(x) + 2Φ(a) − 2, equivalently P(X ≤ x) − Φ(x) ≤ Φ(a) − 1/2. Keller and Klein conjectured the two-sided bound |P(X ≤ x) − Φ(x)| ≤ Φ(a₁) − 1/2 with a₁ the largest coefficient; Ivanisvili's computer-assisted manuscript of 21 October 2026 proves the lower half and the full conjecture for a₁ ≥ 0.07, and leaves this range open. The proof follows the analytic route his manuscript proposes, using Prawitz smoothing, coefficient profiles and a compensated alias estimate. Together with his results it implies the full conjecture, conditionally on those unrefereed external results.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Probability and normal approximation
- Subject
- Discrete analysis, tilings, probability and entropy
- Result type
- Theorem completing an open range and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
keller-klein- Keywords
- Keller–Klein conjecture, Keller-Klein conjecture, Rademacher sums, Berry–Esseen, normal approximation, Kolmogorov distance, Prawitz smoothing, randomly signed sums
Statement and scope
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.
A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.
Manuscript
- PDF on this site
manuscript.pdf364 KB- PDF on GitHub
papers/mathematics/ keller-klein/ manuscript.pdf - LaTeX source
papers/mathematics/ keller-klein/ manuscript.tex
Formal proof
This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.
- Proof package
papers/mathematics/ keller-klein/ - Lean project
papers/63 Lean filesmathematics/ keller-klein/ lean/ - Lakefile
papers/mathematics/ keller-klein/ lean/ lakefile.lean - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
lake exe cache get
python3 verify.py --lean "$(lean --print-prefix)/bin/lean" --mathlib .lake/packages/mathlib- README
papers/mathematics/ keller-klein/ README.md - Verification guide
papers/mathematics/ keller-klein/ verification/ README.md - Verification record
papers/mathematics/ keller-klein/ VERIFICATION.md - Authorship
papers/mathematics/ keller-klein/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Questions and answers
Is the Keller–Klein conjecture now proved?
This preprint proves the upper half of the conjecture when every coefficient is at most a ≤ 7/100, the range left open by Ivanisvili's computer-assisted manuscript of 21 October 2026, which proves the lower half and the case a ≥ 0.07 and proposed the analytic route used here. Together with his Theorems 1.1 and 10.9 it implies the full conjecture, but only conditionally on those unrefereed external results.
What exactly does the paper prove?
For X = Σ vᵢεᵢ with independent uniform signs, real coefficients, Σ vᵢ² = 1 and |vᵢ| ≤ a with 0 < a ≤ 7/100, it proves P(|X| ≤ x) ≤ 2Φ(x) + 2Φ(a) − 2 for every x ≥ 0, equivalently P(X ≤ x) − Φ(x) ≤ Φ(a) − 1/2. Coefficients may be unequal and the number of terms is unrestricted.
Is the proof formally verified?
The stated theorem is formalized in 62 Lean 4 modules, with the exact count of sign vectors and Mathlib's standard normal distribution function. Ivanisvili's results needed for the full conjecture are not formalized, and the work is an unrefereed preprint.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026kellerklein,
author = {Goyal, Dev D.},
title = {The Small-Coefficient Upper Half of the {Keller--Klein} Conjecture},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/keller-klein}
}