In 1995, Ravi Kannan, László Lovász, and Miklós Simonovits conjectured that the best hyperplane cut approximates the optimal isoperimetric bottleneck in a convex body within a universal factor, independent of dimension. In October 2026, several manuscripts claimed a dimension-free bound. I then started a Lean formalization in Codex. Its first completed checkpoint arrived about 23½ hours later.

What KLS says

An isotropic law has mean zero and identity covariance. KLS predicts one universal Poincaré Constant $C>0$ such that, for every dimension $n\ge1$, every isotropic log-concave probability law $\mu$ on $\mathbb{R}^n$, and every locally Lipschitz function $f$ with finite Dirichlet energy, $f\in L^2(\mu)$ and

$$ \operatorname{Var}_\mu(f)\le C\int\|\nabla f\|^2\,d\mu. $$

Here $h(\mu)$ is the Cheeger constant:

$$ h(\mu)=\inf_{0<\mu(A)<1}\frac{\mu^+(A)}{\min\{\mu(A),1-\mu(A)\}}. $$

The infimum runs over Borel sets; $\mu^+(A)$ is the lower limiting probability growth per unit outward Euclidean enlargement. Definition

Equivalently, one universal $c>0$ satisfies $h(\mu)\ge c>0$ for every such law: separating substantial mass requires substantial boundary. The Poincaré Constant and $h(\mu)^{-2}$ are comparable by the Cheeger–Buser theory for log-concave laws. Milman (2009) · De Ponti–Mondino

Uniform laws on convex bodies and Gaussian laws are log-concave. KLS links their geometry to concentration, random sampling, and volume computation.

How the dimension dependence improved

The historical bounds below use $\psi_n=\sup_\mu h(\mu)^{-1}$, with the supremum over all isotropic log-concave probability laws on $\mathbb{R}^n$. Smaller is better. Universal factors are suppressed; the corresponding Poincaré dependence is squared.

Milestone Upper bound for $\psi_n$
KLS, 1995 $O(\sqrt n)$
Eldan, 2013 $O(n^{1/3}\sqrt{\log n})$
Lee–Vempala, 2016 preprint $O(n^{1/4})$
Chen, 2020 preprint $n^{o(1)}$
Klartag–Lehec, 2022; Jambulapati–Lee–Vempala, 2022 $O((\log n)^5)$, then $O((\log n)^{3.2226})$
Klartag, 2023 $O(\sqrt{\log n})$
Letwin, July 2026 $O((\log n)^{1/4})$

Klartag–Lehec's 2025 preprint proved the thin-shell conjecture. Chen–Klartag's July 2026 preprint subsequently obtained the sharp inequality $\operatorname{Var}(|X|^2)\le8n$. Letwin's quadratic estimate supplied a broader input: for isotropic log-concave $X$ and symmetric $M$,

$$ \operatorname{Var}(X^\top M X)\le8\operatorname{Tr}(M^2). $$

In their September 29, 2026 preprint, Dan Mikulincer and Ilias Zadik proved a dimension-free Poincaré bound for isotropic unconditional log-concave laws: laws invariant under changing any coordinate's sign. This settles an important symmetric case of KLS; the general conjecture also covers laws without that symmetry. Here “unconditional” describes a symmetry assumption, whereas my “unconditional formalization” means a proof without an unproved analytic premise.

The September–October breakthroughs and their connections

The manuscript versions matter: Song–Zhang's first version retains a log-star dependence, while its second claims a constant bound. Both versions cite Letwin. The other two October manuscripts explicitly refer to the first version.

Selected version-specific citations among the recent KLS papers.

Solid arrows run from cited work to citing work; the dashed arrow marks a revision. A citation need not be a proof dependency. Dates use arXiv histories, except the GitHub file's first commit; they record public chronology, not discovery priority. The September and October manuscripts disclose AI assistance.

From a Markdown prompt to Lean

The first complete Lean formalization was accomplished in about 24 hours, essentially from one main Markdown prompt. Codex kept working through to completion without routinely stopping for new instructions; my follow-ups were brief progress questions and guidance.

On October 6, I prepared the main prompt and a companion target-search document. GPT-6.1 Sol (Ultra) helped write the brief for GPT-6 Astra (Ultra / Fast). The run began at 12:11 CDT and used GPT-6 Astra (Ultra) → GPT-6.1 Sol (Ultra, then Max); speed settings varied. Model and timing records · Preparation record

The prompt fixed the full isotropic Cheeger and Poincaré endpoints, finite-energy integrability, the optimal-constant definitions, explicit sufficient bounds, and audit requirements. I later deferred finding the sharp constant.

At 15:41 CDT on October 6, I encouraged a literature-informed shortcut. These are exact excerpts from one message:

“You need to first search the literature extensively to identify potentially useful results, without restricting yourself to the original area. Search mathlib/other source what package might already exists.”

“Also search the literature, is there any other way to by pass the current blue print, that is easy short cut for lean to formalize this task, but still lead to the proof of the KLS conjecture exactly.”

“You can adaptively adjust the blue print. Just make the lean formalization task proper in lean. I trust in you. You can do this.”

The system could revise the blueprint while preserving the theorem. The completed chain mainly follows Bizeul–Klartag–Lehec's cumulant, suspension, and Taylor-criterion route, with Letwin's quadratic input and Song–Zhang's endpoint comparison. A weak moment-map argument at $C^{1,1}$ regularity supplied the quadratic seed, avoiding an unused classical-regularity branch. It does not formalize all three papers line by line. Exact follow-ups · Technical report

Multiple agents worked together on proof development and checking. For the local Lean builds, I authorized up to 17 CPU cores on my 2026 Mac with an M5 Pro chip, while the final whole-project replay recorded nine concurrent single-threaded Lean compilers. That authorization is not a measurement of continuous CPU utilization.

What the verified project establishes

The accepted endpoint covers every positive dimension and the full isotropic log-concave class, including nonsmooth laws and unbounded support. Its explicit bounds are

$$ C_P(\mu)\le C_*\le500, \qquad h(\mu)\ge\frac{100}{197\sqrt{500}}. $$

Here $C_*$ is the defined optimal universal Poincaré constant, whose value remains unknown. 500 is a sufficient bound; 1.97 is the Cheeger conversion coefficient. Neither is claimed optimal. Stronger analytic Cheeger–Buser comparisons are known; this article reports the bound formalized in the project. Comparison

The exact combined Lean type is:

KLS.dimensionFree500_and_cheeger197 :
  (∀ (n : ℕ),
      1 ≤ n →
        ∀ (ρ : OAI.LeanBlast.KLS.Space n → ℝ),
          OAI.LeanBlast.KLS.IsLogConcaveDensity ρ →
            OAI.LeanBlast.KLS.IsIsotropic (OAI.LeanBlast.KLS.densityMeasure ρ) →
              OAI.LeanBlast.KLS.PoincareBound (OAI.LeanBlast.KLS.densityMeasure ρ) 500) ∧
    ∀ (n : ℕ),
      1 ≤ n →
        ∀ (μ : MeasureTheory.Measure (KLS.Space n)),
          KLS.admissibleMeasure μ → ENNReal.ofReal (100 / (197 * √500)) ≤ KLS.cheegerConstant μ

Its first component preserves the statement supplied by OpenAI's KLS benchmark, with smooth compactly supported tests inside PoincareBound. The project also proves the locally Lipschitz finite-energy version, including square-integrability. Endpoint source · Definitions and full theorem types

The first checkpoint's replay rebuilt 1,744 proof modules against a pinned Lean/Mathlib foundation cache. The improved endpoint was independently replayed against that baseline. Its saved statement review explicitly checks the type above, the original definitions, quantifier order, and integrability obligations. The audits report only propext, Classical.choice, and Quot.sound, with no sorryAx or added mathematical axiom. Baseline verification · Endpoint receipt · Statement review

These are local checks by the proof system and checking agents, not an external mathematical review. Preparing this blog did not run another Lean build. Earlier bounds remain archived; later optimization is excluded from the first-completion measurements below.

Code, time, and cost

The measurements below use the first completed source checkpoint; later optimization is excluded.

Measure KLS files All project proof modules
Lean files 1,258 1,744
Physical source lines 115,782 263,884
Nonblank lines after removing comments 98,886 216,652
Written theorem / lemma commands 4,995 10,000

The larger totals include supporting and ported libraries, excluding Mathlib and dependency sources. A full recount confirmed 4,995 + 5,005 = 10,000, with no search-result limit. These are source commands, not distinct research theorems. The environment audit separately records 16,956 theorem constants, including private and compiler-generated declarations. Counting method · Recount

The task started October 6 at 12:11:24 CDT; the main agent reported completion October 7 at 11:43:40 CDT: 23 hours, 32 minutes, 16 seconds. The final replay took approximately 33 minutes. Earlier prompt preparation and later constant optimization are excluded; blueprint development inside the run is included. These are elapsed times, not CPU-hours. Timeline

The main chat and its three agents recorded approximately 2.59 billion tokens before completion: 2.53 billion cached input, 52.27 million uncached input, and 9.81 million output. About 97.6% was cached input. The headline measures reused context and model traffic, not billions of newly generated proof tokens. Usage calculation

During the run, I upgraded from the plan I describe as Pro $200 to Pro $500. I reported consuming one weekly allowance on the former, two on the latter, and additional credits.

My subscription allocation was $100 + $250 = $350. The final credit count was 40,000 at $0.04 per credit, costing $1,600. The total cost was $350 + $1,600 = $1,950.

The useful outcome is an inspectable chain connecting a precise theorem to explicit constants, formal proofs, and recorded checks. The initial prompt fixed the destination; the proof route could evolve.