The KLS500 Lean proof targets OpenAI's full KLS statement, but only its author has reported building it, and it does not formalize the recur

What we checked

• Can the repository's Lean sources be independently compiled and shown to formalize the claimed dimension-free KLS bound rather than only supporting lemmas? partly confirmed. The endpoint part holds. KLS500.openaiKLS has type OAI.LeanBlast.KLS.KLSStatement, which is pinned to a hashed commit of openai/math. That statement asserts one constant C>0 such that every isotropic log-concave density in every dimension n≥1 satisfies a Poincaré bound with C. So the endpoint is the full dimension-free statement, not a lemma. Independent compilation is unresolved: I did not build the code, there is no visible CI result, the verification README says 'no independent human semantic review is claimed', and Comparator and Nanoda were not run. [1][3][4][6][12]
• Does the Lean development formalize the Song–Zhang proof described in the headline (a recursive criterion applied repeatedly with errors bounded across iterations)? refuted. The repository and its Zenodo record say the development follows mainly the Bizeul–Klartag–Lehec cumulant-and-suspension approach. It uses only Song and Zhang's tilt–spectral criterion. Microsoft says Song and Zhang's own streamlined Lean verification has not been released yet. [12][11][15]

What we found

• The endpoint is the full theorem, not supporting lemmas. KLS500.lean has a one-line theorem openaiKLS whose type is OAI.LeanBlast.KLS.KLSStatement. It also has poincare500, cheeger197 and universalPoincareRange (4 ≤ C* ≤ 500). Each proof is a call into internal KLS.Final modules. [1][2]
• The target statement comes from OpenAI and is pinned by commit and hash. UPSTREAM.json records openai/math commit adc7f124… and the file lean/OAI/Analysis/KLS/Model.lean with its SHA-256. In that file, KLSStatement says there exists C>0 such that for every n≥1 and every isotropic log-concave density ρ, PoincareBound(densityMeasure ρ) C holds. The test functions are smooth and compactly supported, and isotropy requires explicit moment integrability. openai/math describes itself as manuscripts and proof artifacts produced by an internal OpenAI model, with Lean formal statements and Comparator instructions. [3][4][5]
• All build evidence comes from the author. The verification README says the accepted release rebuilt 1,710 mathematical modules. It also says endpoint axiom closures use only propext, Classical.choice and Quot.sound, and that two new interfaces compiled without warnings. It discloses that this checkout did not get a fresh full rebuild, that cached build outputs are not distributed, that Comparator and Nanoda were not run, and that review was 'self-assessed with agent assistance' with 'no independent human semantic review'. [6][7]
• The repository is small, young and specific to one toolchain. It pins Lean leanprover/lean4:v4.35.0-rc3 and a specific Mathlib commit, and had 5 commits and 1 star when I checked. The sorry scan (final-source-scan.json) shows empty forbidden_tokens lists in the part I could read, but the file does not say which tokens were searched for. Zenodo archived version 1.0.0 on 7 October (University of Minnesota affiliation) and notes that a newer version exists. [8][9][10][11]
• The formalization follows a different proof from the headline's. The README and Zenodo say it follows mainly the Bizeul–Klartag–Lehec cumulant-and-suspension method plus Song and Zhang's tilt–spectral criterion, with the author's own quantitative refinements producing the constant 500. The Bizeul–Klartag–Lehec abstract calls Song and Zhang's criterion 'the crucial step' and notes a paragraph on AI use. Microsoft says Song and Zhang verified a shortened argument in Lean and will release it after final review. [12][13][14][15]
• The three paper proofs give different constants. The Lean development claims 500. Balasubramanian and Kasiviswanathan claim 25 in their v2 abstract and do not mention Lean. Microsoft's post says multiple independent researchers have validated the work, but none of the papers is described as peer-reviewed. [16][15]

What it means

The usual weak point of a Lean claim is whether the final statement says what the paper says, and that part looks solid here. The proof targets a statement written by someone else (OpenAI), pinned by commit and hash, which plainly asserts one dimension-free Poincaré constant for isotropic log-concave densities. Because Poincaré and Cheeger constants are equivalent up to constants for log-concave measures, that is KLS in its standard form. Two caveats remain. The class of densities and test functions is a choice OpenAI made in its formal statement, and no outside human has reviewed it. And every build, sorry-scan and axiom check result is self-reported, made with agent help, without Comparator or Nanoda.

Treat KLS500 as a strong candidate rather than an independent confirmation. To rely on it, run a clean lake exe cache get && lake build on the pinned rc toolchain. Then run #print axioms KLS500.openaiKLS yourself, and run OpenAI's Comparator to check that the vendored Model.lean matches the pinned upstream file. Also keep apart what has been checked: Song and Zhang's iterated recursive argument, the one in the headline, has no public formalization yet. KLS500 checks a different route that relies on their criterion. For AI-for-math pipelines, the pattern to copy is an upstream statement pinned by hash with a mechanical endpoint check. Human sign-off on what the statement means is still needed.

Still open

• Has anyone outside the project rebuilt KLS500 from a clean checkout and confirmed the axiom closure of KLS500.openaiKLS?
• Does OpenAI's Comparator, which was not run, confirm that the vendored statement matches openai/math commit adc7f124 exactly?
• Has a human expert reviewed OpenAI's formal KLSStatement (density-only measures, smooth compactly supported test functions) as faithful to the conjecture?
• When will Song and Zhang release their own streamlined Lean verification, and will it formalize the iterated recursive refinement?