Existing Lean statements of KLS: source search

Search date: October 6, 2026. This search concerns existing formal statements and whether their sources prove them. A conjecture declaration is distinct from a proof.

The concrete existing candidate is KLS.KLSConjecture in Job 45 of brando90/conjecture-prover. No matching KLS declaration was located in the pinned mathlib, Formal Conjectures, or LeanEval snapshots below. No pre-existing Poincaré KLS target was located in those libraries. These are bounded findings, not a claim that no other artifact exists.

Exact existing target

Its mathematical content is

$$ \exists c\in\mathbb R,\ c>0,\quad \forall n\in\mathbb N,\ n\ge1\Longrightarrow \forall\mu:\operatorname{Measure}(\mathbb R^n),\quad \operatorname{IsKLSMeasure}(\mu)\Longrightarrow h(\mu)\ge c. $$

This summarizes the actual declaration; the pinned source contains its exact Lean syntax. The ambient space is KLS.Space n, defined using EuclideanSpace ℝ (Fin n), and the lower bound uses ENNReal.ofReal.

The statement relies on concrete definitions:

Status: source-inspected statement candidate. Its definitional and conditional proof scripts do not prove this proposition unconditionally. This search did not independently compile it or prove its full semantic correspondence. Before freezing it, require a pinned build, a definition audit, nonempty-class examples, and a formal bridge from measure-based log-concavity to its density-based class. Its older literature-status comments should not determine the status of the October preprints.

Source snapshot Search and result
mathlib4 4beb549110aa44b87d699166cece6e3642bddf34 Searched all 9,192 Lean files, including Mathlib, Archive, Wanted, and tests. No matching KLS declaration was located. Poincaré and isotropy name matches concerned other subjects. Relevant public issue/PR searches supplied no KLS target.
Formal Conjectures 89294ea02bd7cd678d59984add52cb4baef3dbf4 Searched all Lean, Markdown, and TOML sources. No KLS or log-concave-measure statement was located. Public KLS/Kannan issue and PR searches found no candidate.
LeanEval 2e58dff1c3d3aa934614d46205e8f430f9a7ca7e Same source scan found no KLS statement. PR #638 instead states Bourgain's slicing result, with an unfinished proof.
AIM c9929805cece044705abaaebe1cebddac1ba11a6 The catalog mentions KLS, but its Lean workspace contains infrastructure and smoke controls rather than an AIM KLS target. Its workspace README explicitly describes the absence of problem targets.

The closed, unmerged mathlib PR #40824 contains a related one-dimensional interval Poincaré inequality. Its declaration is MeasureTheory.lintegral_pow_le_mul_lintegral_pow_deriv_of_integral_eq_zero, in the pinned proposed file. It is not the all-dimensional log-concave KLS statement and is absent from the searched mathlib snapshot.

Additional checks covered public GitHub code searches, the evand/open-math-problems catalog, OpenTorus's KLS campaign, and Reservoir package metadata. These catalog descriptions and campaign plans supplied no exact KLS Lean declaration. GitHub indexing is incomplete: even known files can be absent from keyword results. Package metadata searches do not audit every registered repository's sources.

Recommendation for the prompt

Require both full formulations. Use the pinned KLS.KLSConjecture as the existing Cheeger candidate, subject to the audits above. Define and review a Poincaré companion if no faithful newer upstream declaration is found. Identify that companion as a new formal statement built on audited definitions and mathlib.

Prove every formulation bridge used, with explicit conversion constants. Keep Poincaré and reciprocal-Cheeger constants in separate ledgers. Producing both verified endpoints does not identify their sharp constants with each other.