The Berry–Esseen constant

Upper bound, last-listed row

| $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]. |value changed 2026-09-26

Lower bound, last-listed row

| $c_{E} := \dfrac{\sqrt{10}+3}{6\sqrt{2\pi}} \approx 0.4097321837$ | [E1956] | Esseen’s lower bound; achieved asymptotically by (centered/normalized) Bernoulli sums. |tracked since 2026-07-24 — no movement seen yet

Checked against material for its cited source

• Another row, not one shown above: bound row $0.4748$ line 43 citing [She2011] — the claim we checked: that the cited 2011 reference gives the upper bound this row lists, 0.4748 (the row's comment is empty, so the value is the whole claim). What we read supports it: Corollary 1 states that the classical Berry–Esseen inequality holds with C₀ = 0.4748. source link (read in the arXiv preprint, version 1 (28 Nov 2011), the only version the saved abstract page listed: pp. 1–3, from page images). Selected: drawn by its position in the list of cited rows, not because it looked wrong.
• Another row, not one shown above: bound row $0.82$ line 37 citing [Z1967] — the claim we checked: that Zolotarev's 1967 paper gives the upper bound 0.82 by smoothing inequalities. What we read supports the value and not the method: the paper states the bound 0.82 for identically distributed terms, but announces it without proof, saying the proofs will be published elsewhere, so it does not show that the bound comes from smoothing inequalities. This verdict does not cover whether either bound is proved, since the paper states 0.82 and the comment's 0.9051 without proof. source link (read in the cited journal edition (Z. Wahrscheinlichkeitstheorie verw. Geb. 8, 332–342), from Springer's PDF: pp. 332–334 and 339–342 from page images, with p. 333 re-read in this session from the PDF's text layer; pp. 335–338 were not read). Selected: drawn by its position in the list of cited rows, not because it looked wrong.

2 bound row(s) here have been checked against material for their cited source (2 drawn by position, 0 chosen because something already looked wrong). Across this whole ledger 70 row(s) have been drawn by position, against 691 rows that name a source, counted on 2026-09-27: 64 were checked against material for their cited sources and for 6 the cited source could not be read at all. 5 more were chosen for suspicion and checked; they are counted apart, because a set selected for suspicion carries no rate. A row not listed here has NOT been checked.