I have released KLS15 (https://github.com/HongruZhao/KLS15), an unconditional Lean 4 formalization establishing a dimension-free upper bound of 15 for the Poincaré constant of every isotropic log-concave probability measure: C_P(μ) ≤ 15. The inequality covers all locally Lipschitz L²(μ) functions. The main endpoint is KLS15.poincare15; related endpoints include KLS15.universalPoincareUpper15 and KLS15.openaiKLS.
On October 8, 2026, Balasubramanian and Kasiviswanathan’s revised preprint (https://arxiv.org/abs/2610.07728v2) reported the bound C_P(μ) ≤ 25. Building on their approach, I reduced the upper bound to 15 on October 9. This is a sufficient upper bound; optimality is not claimed.
My earlier KLS500 formalization, which established the bound C_P(μ) ≤ 500, was based chiefly on the Bizeul–Klartag–Lehec cumulant/suspension approach (https://arxiv.org/abs/2610.05474), incorporating the Song–Zhang criterion (https://arxiv.org/abs/2610.01447).
This AI-generated Lean development was carried out under my direction, using ChatGPT GPT-6 Astra (Ultra) for the Lean blueprint and GPT-6.1 Sol (Ultra/Max) for Lean preparation.
Verification: Lean-checked, statement unaudited. The endpoint KLS15.openaiKLS directly uses OpenAI’s unchanged KLSStatement (https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/KLS/Model.lean#L47-L58) as its theorem type, with universal witness 15.
GitHub: KLS15 (https://github.com/HongruZhao/KLS15)
Zenodo: Version 2.0 archive (https://doi.org/10.5281/zenodo.23272815)
Please consider adding this formalization to the existing KLS entry.
I have released KLS15 (https://github.com/HongruZhao/KLS15), an unconditional Lean 4 formalization establishing a dimension-free upper bound of 15 for the Poincaré constant of every isotropic log-concave probability measure: C_P(μ) ≤ 15. The inequality covers all locally Lipschitz L²(μ) functions. The main endpoint is KLS15.poincare15; related endpoints include KLS15.universalPoincareUpper15 and KLS15.openaiKLS.
On October 8, 2026, Balasubramanian and Kasiviswanathan’s revised preprint (https://arxiv.org/abs/2610.07728v2) reported the bound C_P(μ) ≤ 25. Building on their approach, I reduced the upper bound to 15 on October 9. This is a sufficient upper bound; optimality is not claimed.
My earlier KLS500 formalization, which established the bound C_P(μ) ≤ 500, was based chiefly on the Bizeul–Klartag–Lehec cumulant/suspension approach (https://arxiv.org/abs/2610.05474), incorporating the Song–Zhang criterion (https://arxiv.org/abs/2610.01447).
This AI-generated Lean development was carried out under my direction, using ChatGPT GPT-6 Astra (Ultra) for the Lean blueprint and GPT-6.1 Sol (Ultra/Max) for Lean preparation.
Verification: Lean-checked, statement unaudited. The endpoint KLS15.openaiKLS directly uses OpenAI’s unchanged KLSStatement (https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/KLS/Model.lean#L47-L58) as its theorem type, with universal witness 15.
GitHub: KLS15 (https://github.com/HongruZhao/KLS15)
Zenodo: Version 2.0 archive (https://doi.org/10.5281/zenodo.23272815)
Please consider adding this formalization to the existing KLS entry.