David Lorell Releases a Lean Project with a New Version of the Hidden Variable Proof
David Lorell Releases a Lean Project with a New Version of the Hidden Variable Proof
On August 11, David Lorell published a new version of the “natural latent variables” result on LessWrong and linked the post to an open project in Lean, a language and environment in which software checks formal proofs. The authors withdrew their previous proof of the same idea after finding an invalid intermediate step.
In this mathematical problem, two observations may depend on a shared factor that cannot be observed directly, which is called a latent variable. The question is whether, in the approximate setting, a latent variable that includes random noise can be replaced by a rule computed from the pair of observations itself.
In August 2025, Lorell and John Wentworth published a proof of this transition. They later reported that one intermediate step was invalid and that they could not repair the proof. In the new post, Lorell writes that he spent about a month using language models to search for a proof and to perform autoformalization, which means translating the argument into a form that software can verify.
In the pinned version of the project, a single deterministic rule is selected for every finite distribution over a pair of observations. This rule is a function of that pair. According to the stated theorem, it must work with every admissible latent variable that has the same distribution. The error measure of this rule is bounded by the error measure of the stochastic version multiplied by a universal constant less than 1771. Lorell describes this result as stronger than the earlier target.
The repository contains more than the theorem statement. Its verification script searches for incomplete sections and prohibited workarounds, builds the library, and reports which assumptions support the theorems declared in the project. The versions of Lean and its libraries are pinned, so another researcher can run the same verification in the same environment.
The open project separates two checks. Lean determines whether the stated result follows from the chosen definitions and assumptions. Mathematicians must still read the statements to determine whether the formalization matches the original mathematical problem. The code makes the first check reproducible. The second still requires substantive mathematical review.