diff --git a/README.md b/README.md index c2c630f..3087446 100644 --- a/README.md +++ b/README.md @@ -45,7 +45,7 @@ Bounds for which the level of available verification is currently at minimal lev | [16](https://teorth.github.io/optimizationproblems/constants/16a.html) | Brezis–Gallouet–Wainger remainder constant on the 2D torus | $\frac{\beta + \pi}{\pi} \approx 1.82283$ | $\approx 2.15627$ | | [17](https://teorth.github.io/optimizationproblems/constants/17a.html) | Exponential growth constant of diagonal Ramsey numbers | $\sqrt{2} \approx 1.4142$ | 3.7919936995 | | [18](https://teorth.github.io/optimizationproblems/constants/18a.html) | Marton's conjecture constant (PFR) | 1 | 9 | -| [19](https://teorth.github.io/optimizationproblems/constants/19a.html) | Berry–Esseen constant | 0.4097321837 | 0.4690 | +| [19](https://teorth.github.io/optimizationproblems/constants/19a.html) | Berry–Esseen constant | 0.4097321837 | 0.4690 (0.423*) | | [20a](https://teorth.github.io/optimizationproblems/constants/20a.html) | Thin shell conjecture constant | 2 | $< \infty$ | | [20b](https://teorth.github.io/optimizationproblems/constants/20b.html) | Isotropic constant of a log-concave probability measure | $1/e$ | $< \infty$ | | [20c](https://teorth.github.io/optimizationproblems/constants/20c.html) | KLS constant for log-concave probability measures | $\sqrt{\pi/2} \approx 1.25331$ | $\infty$ | @@ -158,6 +158,8 @@ Bounds for which the level of available verification is currently at minimal lev - [15a](https://teorth.github.io/optimizationproblems/constants/15a.html) **improved upper bound:** $C_{15a} \leq 2.371177$ by [E. Dupont, M. Eisenberger, B. Kozlovskii, A. Mehrabian, F. J. R. Ruiz, A. See, R. Zhou, J. Alman, V. Vassilevska Williams, M. Balog](https://arxiv.org/abs/2608.16884), 17 Aug 2026. - [43](https://teorth.github.io/optimizationproblems/constants/43a.html) **improved lower bound (unverified):** $C_{43} \geq 0.860*$ (exact $43/50$; certificate-layer result conditional on the lemma set of [KHSHGW2026](https://arxiv.org/abs/2601.22365)) by [J. Savva](https://doi.org/10.5281/zenodo.22223485), 1 Sep 2026. - [88a](https://teorth.github.io/optimizationproblems/constants/88a.html) **improved upper bound:** $C_{88a} \leq 186$ via $\mathrm{DHL}[40,2]$, by [OpenAI](https://cdn.openai.com/pdf/51126fac-1b68-4128-9666-c908bcc16033/short_gaps.pdf), 30 Aug 2026, with a Lean 4 formalization conditional on three declared axioms. +- [19](https://teorth.github.io/optimizationproblems/constants/19a.html) **improved upper bound (unverified):** $C_{19} \leq 0.4395*$ by [H. Xiao and C. Li](https://github.com/haonan-xiao/iid-berry-esseen), 10 Sep 2026. +- [19](https://teorth.github.io/optimizationproblems/constants/19a.html) **improved upper bound (unverified):** $C_{19} \leq 0.423*$ by [Y. Lin](https://github.com/CoolRmal/BerryEsseen), 13 Sep 2026. ## Maintainers diff --git a/constants/19a.md b/constants/19a.md index 78c7891..de88b2f 100644 --- a/constants/19a.md +++ b/constants/19a.md @@ -42,6 +42,8 @@ This constant is also called the **absolute constant** $C_{0}$ in the Berry–Es | $0.4785$ | [Tyu2009] | | | $0.4748$ | [She2011] | | | $0.4690$ | [She2013] | | +| $0.4395^*$ | [XL2026] | Unverified. GitHub repository with a Lean 4 formalization; its finite certificates are checked with `native_decide`. Uses the shared moment ratio $\mathbb E\lvert X-X'\rvert^3/(2\mathbb E\lvert X\rvert^3)$ and $\mathbb E\lvert X\rvert$ to sharpen the characteristic-function bounds in Prawitz smoothing. | +| $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 @@ -59,11 +61,13 @@ This constant is also called the **absolute constant** $C_{0}$ in the Berry–Es $$ which in particular implies $C_{19}\le 0.4690$. +* **Verification status of the recent bounds:** The bounds $0.4395$ and $0.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 $c_{E}$; see [Sch2016] and references therein. ## References * [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](https://github.com/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). @@ -72,6 +76,7 @@ This constant is also called the **absolute constant** $C_{0}$ in the Berry–Es * [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](https://github.com/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