As a consequence of my #Lean4 formalization project I have found a small (but non-trivial) bug in my paper! While in the course of formalizing the arguments in page 6 of https://arxiv.org/pdf/2310.05328.pdf , I discovered that the expression \( \frac{1}{2} \log \frac{n-1}{n-k-1} \) that appears in those arguments actually diverges in the case \( n=3, k=2\)! Fortunately this is an issue that is only present for small values of \(n\), for which one can argue directly (with a worse constant), so I can fix the argument by changing some of the numerical constants on this page (the arguments here still work fine for \( n \geq 8\), and the small \(n\) case can be handled by cruder methods).

Enclosed is the specific point where the formalization failed; Lean asked me to establish \( 0 < n - 3 \), but the hypothesis I had was only that \( n > 2 \), and so the "linarith" tactic could not obtain a contradiction from the negation of \( 0 < n-3\).

I'll add a footnote in the new version to the effect that the argument in the previous version of the paper was slightly incorrect, as was discovered after trying to formalize it in Lean.