Mathematical formalization in Lean 4

[LeonardoSanBenitez]

Hi, first of all, thank you for work, it's a really nice paper.
I wanted to contribute something I hope is useful to you: I went through the self-contained mathematical results in the paper (the four propositions and the lemma proved in Appendix C, "Proofs") and formalized all of them in Lean 4, using the Mathlib library.

For anyone less familiar with this: Lean is a proof assistant, a language where you write mathematical definitions, theorem statements, and proofs, and a computer mechanically checks that every logical step actually follows, with no room for a hidden gap or an unnoticed mistake. Machine-checked proofs are increasingly used alongside papers precisely because they build a stronger kind of trust than "we checked it by hand and it looks right"; a proof that a computer has verified line by line can't have a mistake that everyone just missed. It's also a solid foundation for anyone, including yourselves, who wants to build on these results later, since it makes completely explicit exactly what has been established and what is still being assumed.

In the lean_proofs/ folder of this PR you'll find Lean formalizations of the paper's mathematical content, one Lean file per result (with a short explanation at the top of each connecting the Lean statement back to your equations):

• The log-sum inequality that all three information-theoretic results rest on, proved from convexity of $t \mapsto t \log t$; from it, KL divergence is non-negative (Gibbs' inequality).
• Lemma 1 — a readout function $f$ can only decrease the KL divergence between the scrubbed distribution and its certificate — proved by applying the log-sum inequality on each level set ${w : f(w) = c}$ and summing over $c$, exactly as in your proof.
• Proposition 1 (Eq. (2)) — the bound $I(Y; f(S(w))) \le \mathbb{E}_{D_f}[\mathrm{KL}(\cdots)]$. The substantive step, $I(X; Z) \le \mathbb{E}_x[\mathrm{KL}(p(z \mid x), \Vert, q)]$ for any reference $q$ with the gap equal to a non-negative KL, is proved in full; the Data Processing Inequality is taken as a hypothesis, exactly as you invoke it as a standard result.
• Proposition 2 — the Local Forgetting Bound (convexity of KL under the seed average), again from the log-sum inequality, applied per outcome over the seed and then summed.
• Proposition 3 — the scrubbing identity $h(A_t(\mathcal{D}, \epsilon)) = A_t(\mathcal{D}_r, \epsilon)$, formalized as the linear-algebra identity relating the two gradient flows; the only property of the matrix exponential it uses is that $e^{At}$ inverts $e^{-At}$, and a second version instantiates this with Mathlib's actual matrix exponential.
• Proposition 4 (isotropic case) — the optimal noise covariance $\Sigma = \sqrt{\lambda \sigma_h^2}, B^{-1/2}$. Instead of the first-order (stationarity) argument, the Lean proof completes the square in the trace inner product, which shows the optimum is a global minimum rather than only a stationary point, and separately verifies your optimality condition $\Sigma B \Sigma = \lambda \Sigma_h$.

The folder has its own README with the full list and instructions for building everything yourself if you'd like to check it independently, and a catalog.json recording, for each result, the paper statement, your own proof, and how the Lean version maps to it. Everything builds with zero unproven steps (sorry is Lean's keyword for an unproven placeholder, and there are none left anywhere), and every result depends only on the standard logical axioms.

One important comment: I relied heavily on Claude Code (Anthropic's AI coding assistant) for this, especially for finding the right building blocks in Lean's math library and writing the proof code. I did go through and check that the statements capture the actual meaning of your results, but since this is your paper and your notation, I'd really appreciate it if you could take a look yourselves and double-check that the Lean statements genuinely capture what you meant, especially for Propositions 3 and 4.

Speaking of which, a few small things came up in Appendix C that look like typos. None of them change any result, but I'd appreciate it if you could confirm them:

• Proposition 3, the map $h$: the middle term is printed $e^{-Bt}(d - d_r)$ in the statement (main text, Eq. (6), and the appendix), but the proof's own final line derives $e^{-Bt}(d_r - d)$. The identity $h(A_t(\mathcal{D}, \epsilon)) = A_t(\mathcal{D}_r, \epsilon)$ holds with $e^{-Bt}(d_r - d)$; with the printed sign it holds only when $d = d_r$. (A quick 1-D check with $w_A^* = 0,\ w_B^* = 1,\ w_0 = 4,\ e^{-At} = e^{-Bt} = 1/2,\ e^{At} = 2$ at $t = 1$ gives $w_B(t) = 2.5$, which the corrected $h$ reproduces and the printed one does not.) The $t \to \infty$ Newton update in Eq. (7) is unaffected, since this term vanishes.
• Proposition 3: the appendix restatement of $h$ drops the leading $w +$ that is present in the main text and in Eq. (6); the proof's final line confirms the $w$ term is present.
• Proposition 4, the KL term: the second factor is printed $(h(w) - h(w'))$; it should be $(h(w) - w')$, so that it equals $\tfrac{1}{2}\mathrm{tr}(\Sigma^{-1} \Sigma_h)$ via $h(w) - w' \sim N(0, \Sigma_h)$.
• Lemma 1, Eq. (10): the rewrite of $\mathrm{KL}(Q \Vert R)$ is printed $\sum_c \sum_{w \in W_c} \log(Q(w)/R(w))$, dropping the leading weight $Q(w)$; the log-sum step needs $\sum_c \sum_{w \in W_c} Q(w) \log(Q(w)/R(w))$.

On the assumptions: a few steps are taken as given rather than derived, and each is marked in the corresponding Lean file. In Proposition 1 the Data Processing Inequality is a hypothesis, as noted above. Proposition 3 formalizes the algebraic identity relating the two flows, taking their closed forms as the paper states them; the $t \to \infty$ Newton update (Eq. (7)) is a limit taken informally in the paper and is not formalized. Proposition 4 formalizes the exact optimization of your own second-order (Gaussian/quadratic) approximate objective — the approximation is assumed, exactly as in the paper — in the isotropic case, and there the symmetric square roots of the positive-definite matrices are taken as hypotheses (they exist by the spectral theorem). Everything else is derived in full.

Once again, thank you for developing this method, I hope these machine-checked proofs are useful to you :)

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.