Executive Summary

Key Figures

The first two numbers give the mathematical gap that closed and the size of the search that found the way through. The last two come from the people who rewrote the result and checked it by machine.

Sources: arXiv 2610.01447 (Song and Zhang), arXiv 2610.05474 (Bizeul, Klartag and Lehec), KLS500 Lean 4 repository

Take a lump of something and cut it in two. The smaller the cut surface, the better the cut. Two knives are available for the job. One is flat and comes down in a single straight stroke. The other bends freely to follow the shape and finds the most efficient surface. That the second cuts better is obvious. The question is how much better.

The conjecture Ravi Kannan, László Lovász and Miklós Simonovits put forward in 1995 says the flat knife's cut surface is larger than the bending knife's by no more than a single universal factor. The condition attached at the end is the heart of it. No matter what the dimension is. In two dimensions or in a million, the flat knife falls behind the bending knife by the same fixed factor. The objects in question are isotropic log-concave distributions, meaning probability distributions that are thick in the middle, thinner toward the edges, and scaled so that the spread measured along any direction comes out the same.

This ratio matters because it governs the speed of a random walk. To draw a point at random from a region you walk around inside it and gather samples, and if the region has a narrow neck somewhere, the walk fails to pass through and gets trapped on one side. The KLS constant bounds how narrow that neck can be. Song and Zhang write that the constant governs the complexity of sampling, volume computation and log-concave integration, and that convex optimization algorithms rest on it as well. The Mathematical Sciences Research Institute called it the central open problem in high-dimensional convex geometry in its 2017-18 annual report.

It helps to know in advance that the same conjecture travels under different names in different fields. The introduction to the 32-page proof sets it out in three equivalent forms. There is the concentration form, where the probability that a function's value strays from its mean falls off exponentially with distance. There is the Poincaré inequality form, where the variance of a function is at most a constant times the integral of its squared gradient. And there is the isoperimetric form, where the area of the surface dividing a region is proportional to the volume it cuts off. The three say the same thing and differ only in the value of the universal constant. So when the Poincaré constant or the Cheeger constant turns up below, read it not as a separate measure but as a quantity that moves with the KLS constant up to a constant factor.

Over 31 years the upper bound came down in steps. Song and Zhang set that staircase out as a table in their first section.

The whole of the new result is that n has vanished from the last row. The log^1/4 n in the row just above also grows very slowly as the dimension rises and is near enough a constant for practical purposes, but what the conjecture demanded was a value entirely free of the dimension. Microsoft summed the consequence up by saying that a range of results that had been assuming the conjecture can now be stated unconditionally.

At the very end of the Song and Zhang paper sits a paragraph recording how the work proceeded, dates included. Lay that paragraph over the arXiv submission dates of the three papers and the Microsoft blog, and the schedule comes back like this.

The October 4 row is the odd one in this story. On the very day Song and Zhang posted the completed proof as their second version, a separately written proof by Bizeul, Klartag and Lehec went up alongside it. The later paper borrows the criterion carried in Song and Zhang's first version and calls it the crucial step in the proof. So the two papers were not competing; they were running a relay. The first set a new criterion at the end of 140 pages and more than 100 attempted routes, and the second took that criterion as its starting line and rewrote the argument in 32 pages.

The criterion that was handed over is worth setting down. Tilt a distribution in one direction, take the average of a function again, and you get a quantity called a tilt average. How sharply that quantity bends as the tilt grows stronger is measured by its higher-order derivatives, and as long as that growth stays within a fixed ratio at every order, the Poincaré constant is bounded independently of the dimension too. That is the criterion Song and Zhang established. Because it replaces a direct assault on the conjecture with a single condition that can be checked, the 32-page paper could put everything into actually satisfying that condition. The final step used suspension. Attach one more coordinate holding independent copies of the distribution to raise the dimension, then carry a cumulant estimate computed in the larger space back to the tilt averages of the original.

A third proof went up on October 6. Like the two before it, the first version built a dimension-free bound on stochastic localization, and the second version two days later replaced that part with a deterministic variational argument that pinned the Poincaré constant at 25 or below. The 25 usually quoted alongside this paper is the value in the second version, not the first. The Microsoft blog says this third proof also appeared on the same day as the other two, but the arXiv record puts it two days later. This article follows the arXiv record.

Machine verification came last. The Lean 4 repository KLS500, published by Hongru Zhao, takes the cumulant and suspension route of Bizeul, Klartag and Lehec as its frame, slots the Song and Zhang criterion into it, and uses a proof assistant to confirm the inequality bounding the variance by 500 times the integral of the squared gradient. This is not a verification that a mathematician reads and accepts, but one a computer follows step by logical step. The repository reports rebuilding 1,710 modules at trust level zero, with the axiom check at the end points turning up only the three standard axioms. With that, the optimal constant has been brought into the interval between 4 and 500.

The item the repository puts at the bottom of its declaration list is of a different kind. It records that the same constant of 500 also passed for the KLS conjecture statement written out in the mathematics repository OpenAI published, which is to say for a proposition the person running the verification did not write. In machine verification, what you took as the proposition to prove matters as much as what you proved. If the party doing the proving also writes the statement, the machine will pass the pair even when both drift together. That is why a second run against someone else's statement was recorded separately.

Three first-hand records carry this story: the Song and Zhang paper, the Bizeul, Klartag and Lehec paper, and the Microsoft blog. All three say they used AI, and what they say does not overlap.

3.1The record that names the tools and the dates

The last section of the Song and Zhang paper is titled "Acknowlegements and AI Disclosure", with the missing letter as it appears in the original. After the thanks comes a single sentence: "The AI tools used in this work were GPT-6 Astra, GPT-5.6 Sol, Claude Fable 5, and Fable 5.1." Four specific model names sit in the body of the paper.

The paragraph that follows reads like a research log. The first author learned of the problem while visiting the University of Washington nearly a decade ago, tried again as a postdoc at the Institute for Advanced Study around 2019 to 2020 and once more from roughly 2022 to 2024, and did not succeed. Then comes the account of testing more than 100 approaches from July 28, with one line on the division of labor attached to it. Candidate approaches were generated collaboratively, with the authors deciding which ones to prioritize.

The section closes with two sentences. All of the proofs have been carefully verified by the authors and several AI tools, and the authors take full responsibility for the correctness of the proofs. The fact of having used the tools and the location of the responsibility are set down separately in the same place.

3.2The record that states the size of the contribution

The 32-page proof filled in a different box. Its arXiv comment field says in advance that the paper runs to 32 pages and contains a paragraph describing AI use. That is the line a reader meets in the listing before opening the paper at all.

The paragraph itself is in the acknowledgements, and it reads as follows. Most proofs and mathematical ideas in the paper were found by ChatGPT; a notable exception is the idea to use suspension, which was suggested by the authors; and the role of the authors has been mostly to understand these proofs and improve their exposition. One model name, ChatGPT, with no version number and no date. What the paragraph gives instead is who did how much.

The first sentence of the introduction catches the eye once more, because it says the KLS conjecture poses little challenge for contemporary AI tools. A reason comes attached to that sentence, though: given the remarkable progress in our understanding of high-dimensional convex bodies in recent decades. Read after the 31 years of steps in the table, the sentence sounds less like a boast than like a citation.

3.3The record that describes the procedure

The Microsoft blog never once names a model. Only common nouns appear, such as AI agents and several leading AI models. What it gives in detail is the procedure. Several agents explored variations on one idea in parallel while the researchers inspected intermediate results, pruned the unpromising directions and passed the most promising ones into the next round. The blog also split the roles in two. AI tools helped explore candidate approaches, carry out detailed derivations, prepare the manuscript and perform internal proof checks, while the researchers determined the mathematical direction, selected the promising ideas, assembled them into the final argument and verified the proof.

One piece of material exists only in the blog. In a separate track of the same project, the authors made repeated unguided attempts at the same problem with several leading AI models, using roughly the same total token budget as the main process, and that effort fell short of the goal. It is a control experiment that appears in neither paper.

Put the three records side by side and the box each one left empty becomes visible. The Song and Zhang paper records what was used, with names and dates, and leaves the size of the contribution empty. The 32-page proof records how much was handed over and leaves version numbers and dates empty. The Microsoft blog records how it was used and leaves the model names empty. Read any one of them on its own and there is no way to learn the other two boxes.

The order of things is worth noticing. The largest acknowledgement of AI's contribution came not from the AI company's blog but from a 32-page paper by three mathematicians outside the company. The model names, likewise, were printed not by the company blog but by the paper that blog introduced. So "undisclosed model names" is the wrong description of this episode. The question is not whether they were disclosed, but in which document and in what form.

One reason the three records diverged is simple. No common form fixes the items that have to be recorded. Journals have begun setting policies that require AI use to be declared, but what to write and to what level of detail is left to the authors. The result is that three documents produced within the same ten days each took one item out of tool names, size of contribution and search procedure.

High-dimensional geometry is not what Pebblous works on. Yet the shape of the record these ten days left behind is the same shape we meet every day in the work of verifying data quality. Once someone is handed an output made with AI, the questions they ask are always the same three. What was used, how much was handed over, how was it used.

Mathematics has a last resort that works even when all three are blank. A proof can be inspected on its own terms, so that knowing nothing of the process, you follow the result line by line and it comes out either true or false. Two independent proofs and the Lean 4 verification did exactly that job this time. The conclusion held even where the disclosure was thin.

Data work rarely has such a last resort. Suppose you receive a dataset where AI attached the labels, filled the gaps and took out the outliers. Staring at the numbers will not tell you which values are original and which are generated. There is no way for the dataset to check itself the way a proof does, so the only path left is to receive the process as a record. That is why answers to the three questions have to arrive together with the output.

• What was used. The tools, the version numbers and the dates. This is the box Song and Zhang filled with four names and a chronology, and because the same model gives different results once the version changes, it is the starting point for reproduction
• How much was handed over. Where the AI's share ends and human judgment begins. This is the box the 32-page paper filled by singling out the suspension idea as its exception, and it tells a reviewer which passages to doubt harder
• How it was used. How candidates were generated and on what grounds they were pruned. This is the box Microsoft filled with its pruning procedure, and it decides whether the same method can be carried over to another problem

What matters about the three boxes is that the last two cannot be restored once the work is finished. The names of the tools can be written down later, but what the 100 discarded routes were and why they were discarded disappears unless it is written at the time. The line dividing the human share from the AI share is sharp only while the work is under way. Once it ends, only the finished object remains, and the finished object does not say who took which part.

The last sentence of the Song and Zhang paper is the most practical thing here. That the authors take full responsibility for the correctness of the proofs holds regardless of how much AI was used. However long the list of tools runs, responsibility for a wrong result does not move across. Disclosure is not a device for dividing responsibility, but a device for keeping open the road by which the next person verifies.

Thank you for reading this far. The figures and quotations in this article were checked directly against the Microsoft Research blog post, the second version of arXiv 2610.01447 and the first version of 2610.05474, the abstract of 2610.07728, and the KLS500 repository description. When an AI-made output is handed to you inside your own organization, we would like to hear what you ask to come with it.

Pebblous Data Communication Team
October 24, 2026

Academic Papers

• 1.Song, Z. & Zhang, X. (2026). "An O(1) Bound for the KLS Constant." arXiv:2610.01447 (v2, 2026-10-04).
• 2.Bizeul, P., Klartag, B. & Lehec, J. (2026). "Presenting a proof of the Kannan-Lovasz-Simonovits conjecture." arXiv:2610.05474.
• 3.Balasubramanian, K. & Kasiviswanathan, S. (2026). "A Dimension-Free Bound on the Poincaré Constant of Isotropic Log-Concave Measures." arXiv:2610.07728 (v2, 2026-10-08).

Official Announcement & Tooling

• 4.Microsoft Research. (2026). "Solving a 31-year-old grand challenge in mathematics: The KLS conjecture." Microsoft Research Blog, 2026-10-21.
• 5.Zhao, H. (2026). "KLS500 — Lean 4 formalization of the KLS conjecture." GitHub.