OpenFrontiers
Join
← Back to the index
OP-12022OpenProbability

Berry–Esseen constant (C19C_{19})

Berry–Esseen constant: determine C19C_{19} or improve its bounds; the repository records 0.4097321837 (lower) and 0.4690 (0.423*) (upper).

MSC 60F05 · Central limit and other weak theorems

Editorial MSC2020 classification. Original article codes and source evidence are recorded in the literature directory.

Licensed source statementAs of Repository table at commit 2c1968c (2026-09-26); open while the recorded lower and upper bounds differSource & evidence ↓
Read original source ↗ 0Submit progressLean 4 ↓Discussion (0)

Problem statement

Let X1,X2,…X_{1},X_{2},\dots be i.i.d. real random variables with EX1=0\mathbb E X_{1} = 0, Var(X1)=1\mathrm{Var}(X_{1})=1, and finite third absolute moment

β3:=E∣X1∣3<∞.\beta_{3} := \mathbb E|X_{1}|^3 < \infty.

Let

Sn:=X1+⋯+Xnn,Fn(x):=P(Sn≤x),S_n := \frac{X_{1}+\cdots+X_{n}}{\sqrt n},\qquad F_n(x):=\mathbb P(S_n\le x),

and let Φ\Phi denote the standard normal distribution function.

We define C19C_{19} to be the smallest constant such that the classical Berry–Esseen inequality

Δn:=sup⁡x∈R∣Fn(x)−Φ(x)∣ ≤ C19 β3nfor all n≥1\Delta_n := \sup_{x\in\mathbb R}\bigl|F_n(x)-\Phi(x)\bigr| \ \le\ C_{19}\,\frac{\beta_{3}}{\sqrt n} \qquad\text{for all } n\ge 1

holds for all such distributions of X1X_{1}.

This constant is also called the absolute constant C0C_{0} in the Berry–Esseen inequality (for i.i.d. summands).

Lean 4

Not yet attached

No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.

Share a formalization →Verification guide ↗

Background

  • Zolotarev’s conjecture: It is conjectured that C19=cEC_{19}=c_{E}, i.e. the Esseen lower bound is sharp. This is sometimes attributed to Zolotarev (1967). See e.g. [vB1972], [KS2009], [Tyu2009] for discussion.
  • How the bound 0.46900.4690 is obtained: Shevtsova [She2013] proves the structural estimate
Δn≤1nmin⁡{0.4690,β3, 0.3322(β3+0.429), 0.3031(β3+0.646)},\Delta_n \le \frac{1}{\sqrt n}\min\bigl\{0.4690,\beta_{3},\ 0.3322(\beta_{3}+0.429),\ 0.3031(\beta_{3}+0.646)\bigr\},

which in particular implies C19≤0.4690C_{19}\le 0.4690.

  • Verification status of the recent bounds: The bounds 0.43950.4395 and 0.4230.423 are established in GitHub repositories with Lean 4 formalizations. In both, the finite numerical certificates are checked with native_decide, so the proofs additionally trust Lean's compiler; neither has been run through leanprover/comparator, and as of this writing neither appears in a peer-reviewed publication.
  • Binomial/Bernoulli case: In the special case of i.i.d. Bernoulli summands (equivalently, binomial distributions after normalization), the optimal constant is known to equal cEc_{E}; see [Sch2016] and references therein.

References (from the repository page)

  • [E1956] Esseen, Carl-Gustav. A moment inequality with an application to the central limit theorem. Skand. Aktuarietidskr. 39 (1956), 160–170.
  • [Lin2026] Lin, Yongxi. Berry–Esseen bounds in Lean. GitHub repository CoolRmal/BerryEsseen (2026); proof document paper/upper-0423.pdf. Developed with AI assistance.
  • [KS2009] Korolev, V. Yu.; Shevtsova, I. G. On the upper bound for the absolute constant in the Berry–Esseen inequality. Teor. Veroyatn. Primen. 54 (2009), no. 4, 671–695 (English transl.: Theory Probab. Appl. 54 (2010), no. 4, 638–658).
  • [Sch2016] Schulz, Jona. The optimal Berry–Esseen constant in the binomial case. PhD thesis, Universität Trier (2016).
  • [She2006] Shevtsova, I. G. A refinement of the upper estimate of the absolute constant in the Berry–Esseen inequality. Teor. Veroyatn. Primen. 51 (2006), no. 3, 622–626 (English transl.: Theory Probab. Appl. 51 (2007), 549–553).
  • [She2011] Shevtsova, Irina. On the absolute constants in the Berry–Esseen type inequalities for identically distributed summands. arXiv:1111.6554 (2011).
  • [She2013] Shevtsova, I. G. On the absolute constants in the Berry–Esseen inequality and its structural and nonuniform improvements. Inform. Primen. 7 (2013), no. 1, 124–125.
  • [Shi1986] Shiganov, I. S. Refinement of the upper bound of the constant in the central limit theorem. J. Soviet Math. 35 (1986), 2545–2550.
  • [Tyu2009] Tyurin, I. S. New estimates of the convergence rate in the Lyapunov theorem. arXiv:0912.0726 (2009).
  • [vB1972] van Beek, Paul. An application of Fourier methods to the problem of sharpening the Berry–Esseen inequality. Z. Wahrscheinlichkeitstheorie verw. Geb. 23 (1972), 187–196.
  • [XL2026] Xiao, Haonan; Li, Chunlin. A 0.4395 upper bound for the i.i.d. Berry–Esseen constant. GitHub repository haonan-xiao/iid-berry-esseen (2026).
  • [Z1967] Zolotarev, V. M. A sharpening of the inequality of Berry–Esseen. Z. Wahrscheinlichkeitstheorie verw. Geb. 8 (1967), 332–342.

Acknowledgements

Prepared with ChatGPT 5.2 Pro.

Progress & source assessment

Repository table (commit 2c1968c, 26 September 2026): best known lower bound 0.4097321837; best known upper bound 0.4690 (0.423*). Values marked with an asterisk have minimal verification.

Known upper bounds

Bound Reference Comments
0.820.82 [Z1967] Zolotarev-type smoothing inequalities; [Z1967] also gives 0.90510.9051 for the general (non-i.i.d.) case.
0.79750.7975 [vB1972] Fourier-analytic refinement.
0.76550.7655 [Shi1986]
0.70560.7056 [She2006]
0.51290.5129 [KS2009] From the structural bound Δn≤0.34445(β3+0.489)/n\Delta_{n} \le 0.34445(\beta_{3}+0.489)/\sqrt n.
0.47850.4785 [Tyu2009]
0.47480.4748 [She2011]
0.46900.4690 [She2013]
0.4395∗0.4395^* [XL2026] Unverified. GitHub repository with a Lean 4 formalization; its finite certificates are checked with native_decide. Uses the shared moment ratio E∣X−X′∣3/(2E∣X∣3)\mathbb E\lvert X-X'\rvert^3/(2\mathbb E\lvert X\rvert^3) and E∣X∣\mathbb E\lvert X\rvert to sharpen the characteristic-function bounds in Prawitz smoothing.
0.423∗0.423^* [Lin2026] Unverified. GitHub repository with a Lean 4 formalization (berryEsseenConstant ≤ 0.423); its finite certificates are checked with native_decide. Builds on the analytic framework of [XL2026]; does not use [She2013].

Known lower bounds

Bound Reference Comments
cE:=10+362π≈0.4097321837c_{E} := \dfrac{\sqrt{10}+3}{6\sqrt{2\pi}} \approx 0.4097321837 [E1956] Esseen’s lower bound; achieved asymptotically by (centered/normalized) Bernoulli sums.
References
  1. [1]Davis, Damek; Ivanisvili, Paata; Tao, Terence (maintainers). Optimization Constants in Mathematics, github.com/teorth/optimizationproblems (commit 2c1968c, 26 September 2026). — Berry–Esseen constant ($C_{19}$) linkApache-2.0 (repository license); constant pages reproduced with attribution; repository references retained.

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Sign in to run an attempt. New accounts start with enough credits for ten.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.

Sign in to add a note.