HEXAGONbeta

The sharp iid Berry–Esseen inequality: Analytic reductions and exact certificate proof

Primarily AI-generated textHuman understanding: some partsmath.PR — Probability

Contributed by Kacper Rodziewicz ↗, Bartosz Kołodziejek ↗

Version 1 / Oct 29, 2026 / CC BY 4.0

Abstract

Let X1,X2,…X_1, X_2, \dots be independent and identically distributed real random variables with E[X1]=0\mathbb{E}[X_1] = 0, E[X12]=1\mathbb{E}[X_1^2] = 1, and finite third absolute moment ρ=E∣X1∣3<∞\rho = \mathbb{E}|X_1|^3 < \infty. Write Fn(x)=P((X1+⋯+Xn)/n≤x)F_n(x) = \mathbb{P}((X_1 + \cdots + X_n)/\sqrt{n} \le x) and let Φ\Phi denote the standard normal distribution function. Define \[ \Delta_n = \sup_{x \in \mathbb{R}} |F_n(x) - \Phi(x)|, \qquad C_n = \sup \frac{\sqrt{n}\,\Delta_n}{\rho}, \qquad C^* = \sup_{n \ge 1} C_n, \] and let \[ C_{\mathrm{E}} = \frac{3 + \sqrt{10}}{6\sqrt{2\pi}} \approx 0.4097321837 \] denote Esseen's 1956 two-point lower-bound constant. We present a computer-assisted proof architecture and complete verification suite establishing unconditionally that \[ C_n \le C_{\mathrm{E}} \quad \text{for every } n \ge 1, \qquad C^* = C_{\mathrm{E}}. \] The proof combines a regularized Prawitz smoothing inequality, a conserved zero-bias/characteristic-function reduction on the all-nn tail, and exact finite verification certificates across 13 roles covering all n≥1n \ge 1 (`full_pass: "ESTABLISHED"`). All certificates, native C++/Python checkers, and a single-command multi-core Docker verification setup (`git clone https://github.com/rodziewiczk/berry-esseen-certificates.git && cd berry-esseen-certificates && docker compose up --build --abort-on-container-exit`) are publicly archived at https://github.com/rodziewiczk/berry-esseen-certificates (tag `v1.0.0-full-pass`).

Provenance statement

AI tools (OpenAI GPT / Codex and Google Gemini / Antigravity) were used for verification engineering, certificate orchestration, manuscript drafting, and audit automation. All mathematical reductions, certificate schemas, and verification executions were directed and verified by the human authors. Reproducible via a single-command Docker container at https://github.com/rodziewiczk/berry-esseen-certificates.
AI provenance filesai-provenance.txt · 1 KB

References

  1. BerryEsseenLean : Berry--Esseen eventual sharpness in Lean . Lean 4 formalization accompanying the manuscript of Hengzhi He and Guang Cheng, 2026. URL https://github.com/UCLA-Trustworthy-AI-Lab/BerryEsseenLean/tree/2b97fa7400dd85fc98b829224c89b0f986789395. Commit 2b97fa7400dd85fc98b829224c89b0f986789395; designated endpoints retain explicit external mathematical inputs; Lean v4.28.0.link
  2. Logan Bell. Extremizers for the independent Berry--Esseen inequality. Manuscript dated 2026-10-06; collection version 0.7.0; source snapshot f61bc638774bfa1165065462f98fe31efade30bf, 2026 a . URL https://github.com/epicycloids/independent-berry-esseen-bounds/blob/f61bc638774bfa1165065462f98fe31efade30bf/paper/extremizers/extremizers.pdf.link
  3. Logan Bell. Berry--Esseen bounds for two summands and Bernoulli arrays. Manuscript dated 2026-10-06; collection version 0.7.0; source snapshot f61bc638774bfa1165065462f98fe31efade30bf, 2026 b . URL https://github.com/epicycloids/independent-berry-esseen-bounds/blob/f61bc638774bfa1165065462f98fe31efade30bf/paper/finite-arrays/finite-arrays.pdf.link
  4. Logan Bell. An upper bound on the Berry--Esseen constant for independent summands. Manuscript dated 2026-10-06; collection version 0.7.0; source snapshot f61bc638774bfa1165065462f98fe31efade30bf, 2026 c . URL https://github.com/epicycloids/independent-berry-esseen-bounds/blob/f61bc638774bfa1165065462f98fe31efade30bf/paper/independent-berry-esseen.pdf.link
  5. Logan Bell. The sharp Berry--Esseen bound for independent arrays with small Lyapunov ratio. Manuscript dated 2026-10-06; collection version 0.7.0; source snapshot f61bc638774bfa1165065462f98fe31efade30bf, 2026 d . URL https://github.com/epicycloids/independent-berry-esseen-bounds/blob/f61bc638774bfa1165065462f98fe31efade30bf/paper/small-lyapunov/small-lyapunov.pdf.link
  6. Logan Bell. On the structural conjecture for extremizers of the independent Berry--Esseen inequality. Manuscript dated 2026-10-18; collection version 0.7.0; source snapshot f61bc638774bfa1165065462f98fe31efade30bf, 2026 e . URL https://github.com/epicycloids/independent-berry-esseen-bounds/blob/f61bc638774bfa1165065462f98fe31efade30bf/paper/structural-conjecture/structural-conjecture.pdf.link
  7. Logan Bell. Zero-bias transport and extremal Bernoulli arrays. Manuscript dated 2026-10-06; collection version 0.7.0; source snapshot f61bc638774bfa1165065462f98fe31efade30bf, 2026 f . URL https://github.com/epicycloids/independent-berry-esseen-bounds/blob/f61bc638774bfa1165065462f98fe31efade30bf/paper/transport/transport.pdf.link
  8. Andrew C. Berry. The accuracy of the Gaussian approximation to the sum of independent variates. Transactions of the American Mathematical Society , 49 0 (1): 0 122--136, 1941. 10.1090/S0002-9947-1941-0003498-3.DOI
  9. P. Erd ő s. On a lemma of Littlewood and Offord . Bulletin of the American Mathematical Society , 51 0 (12): 0 898--902, 1945. 10.1090/S0002-9904-1945-08454-7.DOI
  10. Carl-Gustav Esseen. On the Liapunoff limit of error in the theory of probability. Arkiv f ö r Matematik, Astronomi och Fysik , 28A 0 (9): 0 1--19, 1942.
Show all 35 referencesShow fewer references
  1. Carl-Gustav Esseen. Fourier analysis of distribution functions. A mathematical study of the Laplace--Gaussian law. Acta Mathematica , 77: 0 1--125, 1945. 10.1007/BF02392223.DOI
  2. Carl-Gustav Esseen. A moment inequality with an application to the central limit theorem. Scandinavian Actuarial Journal , 1956 0 (2): 0 160--170, 1956. 10.1080/03461238.1956.10414946.DOI
  3. Larry Goldstein and Gesine Reinert. Stein 's method and the zero bias transformation with application to simple random sampling. The Annals of Applied Probability , 7 0 (4): 0 935--952, 1997. 10.1214/aoap/1043862419.DOI
  4. Hengzhi He and Guang Cheng. The Berry--Esseen constant conjecture is eventually true, 2026. URL https://arxiv.org/abs/2609.06358v3. Version 3, revised 30 September 2026.link
  5. Christian Hipp and Lutz Mattner. On the normal approximation to symmetric binomial distributions. Theory of Probability and its Applications , 52 0 (3): 0 516--523, 2008. 10.1137/S0040585X97983213. Original edition: Teoriya Veroyatnostei i ee Primeneniya 52 (2007), 610--617.DOI
  6. Victor Yu. Korolev and Irina G. Shevtsova. On the upper bound for the absolute constant in the Berry--Esseen inequality. Theory of Probability and its Applications , 54 0 (4): 0 638--658, 2010. 10.1137/S0040585X97984449. English translation of the Russian article published in 2009.DOI
  7. Yongxi Lin. Berry--Esseen bounds in Lean . GitHub repository, 2026. URL https://github.com/CoolRmal/BerryEsseen. Accompanying proof document: The i.i.d. Berry--Esseen constant is at most 0.423: a machine-checked proof, 13 September 2026, paper/upper-0423.pdf. Commit bfb22608ad18b4fa9fda8dd9a1ed2c2b6fbc29e7; accessed 27 October 2026.link
  8. D. Lubell. A short proof of Sperner 's lemma. Journal of Combinatorial Theory , 1 0 (2): 0 299, 1966. 10.1016/S0021-9800(66)80035-2.DOI
  9. Håkan Prawitz. Limits for a distribution, if the characteristic function is given in a finite domain. Scandinavian Actuarial Journal , 1972 0 (2): 0 138--154, 1972. 10.1080/03461238.1972.10404645.DOI
  10. Kacper Rodziewicz and Bartosz Kołodziejek. Moment defects and sharp iid Berry--Esseen bounds. Hexagon preprint hexagon:2610.00147v3, 2026. URL https://hexagonmath.org/2610.00147v3. Working draft, version 3, 17 October 2026; accessed 27 October 2026.hexagon
  11. Jona Schulz. The optimal Berry--Esseen constant in the binomial case . PhD thesis, Universit ä t Trier, 2016. URL https://ubt.opus.hbz-nrw.de/frontdoor/index/index/docId/732.link
  12. Irina Shevtsova. On the absolute constants in the Berry--Esseen type inequalities for identically distributed summands, 2011. URL https://arxiv.org/abs/1111.6554v1.link
  13. Irina Shevtsova. Moment-type estimates with asymptotically optimal structure for the accuracy of the normal approximation. Annales Mathematicae et Informaticae , 39: 0 241--307, 2012. URL https://ami.uni-eszterhazy.hu/uploads/papers/finalpdf/AMI_39_from241to307.pdf.link
  14. Irina Shevtsova. On the accuracy of the approximation of the complex exponent by the first terms of its Taylor expansion with applications. Journal of Mathematical Analysis and Applications , 418 0 (1): 0 185--210, 2014. 10.1016/j.jmaa.2014.03.075. URL https://arxiv.org/abs/1301.2783v3.DOI
  15. Irina G. Shevtsova. Sharpening of the upper bound of the absolute constant in the Berry--Esseen inequality. Theory of Probability and its Applications , 51 0 (3): 0 549--553, 2007. 10.1137/S0040585X97982591. English translation of the Russian article published in 2006.DOI
  16. Irina G. Shevtsova. On the absolute constants in the Berry--Esseen inequality and its structural and nonuniform improvements. Informatics and its Applications , 7 0 (1): 0 124--125, 2013. URL https://www.mathnet.ru/eng/ia252. In Russian.link
  17. I. S. Shiganov. Refinement of the upper bound of the constant in the central limit theorem. Journal of Soviet Mathematics , 35: 0 2545--2550, 1986. 10.1007/BF01121471. English translation of the Russian original, 1982, pp. 109--115.DOI
  18. Terence Tao and contributors . The Berry--Esseen constant. Optimization Constants in Mathematics, Problem 19a, 2026. URL https://github.com/teorth/optimizationproblems/blob/e95af44bc6ae938f545a0fc62cd1b6c1f6088a56/constants/19a.md. Repository snapshot e95af44bc6ae938f545a0fc62cd1b6c1f6088a56; accessed 27 October 2026.link
  19. I. S. Tyurin. Refinement of the upper bounds of the constants in Lyapunov 's theorem. Russian Mathematical Surveys , 65 0 (3): 0 586--588, 2010. 10.1070/RM2010v065n03ABEH004688.DOI
  20. Ilya Tyurin. New estimates of the convergence rate in the Lyapunov theorem, 2009. URL https://arxiv.org/abs/0912.0726v1.link
  21. Paul van Beek. An application of Fourier methods to the problem of sharpening the Berry--Esseen inequality. Zeitschrift f ü r Wahrscheinlichkeitstheorie und Verwandte Gebiete , 23: 0 187--196, 1972. 10.1007/BF00536558.DOI
  22. Haonan Xiao and Chunlin Li. A 0.4395 upper bound for the i.i.d. Berry--Esseen constant. GitHub repository, 2026. URL https://github.com/haonan-xiao/iid-berry-esseen. Accompanying paper: paper/berry-esseen-04395.pdf. Commit f00d781c8c42908bf4aef2739129442a0919fa38; accessed 27 October 2026.link
  23. Asher Yan. ProbabilityApproximation : Berry--Esseen bounds for independent sums. Lean 4 software, release v0.9.6, 2026. URL https://github.com/Polarnova/ProbabilityApproximation/releases/tag/v0.9.6. Commit c89fba908a33ba741836407f43c67609e2d05279; Lean and Mathlib v4.32.0. Cite the original mathematical sources for theorems used.link
  24. Vladimir M. Zolotarev. An absolute estimate of the remainder term in the central limit theorem. Theory of Probability and its Applications , 11 0 (1): 0 95--105, 1966. 10.1137/1111005.DOI
  25. Vladimir M. Zolotarev. A sharpening of the inequality of Berry--Esseen . Zeitschrift f ü r Wahrscheinlichkeitstheorie und Verwandte Gebiete , 8: 0 332--342, 1967. 10.1007/BF00531598.DOI

Version history

  1. v1Submitted by Kacper RodziewiczInitial depositCurrentOct 27, 2026