Skip to content

C_19: record the unverified upper bounds 0.4395 and 0.423 #188

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
CoolRmal wants to merge 1 commit into
base: main
Choose a base branch
from
+8 −1
Open

C_19: record the unverified upper bounds 0.4395 and 0.423 #188

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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$ |
Expand Down Expand Up @@ -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

Expand Down
5 changes: 5 additions & 0 deletions constants/19a.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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).
Expand All @@ -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
Expand Down