Lean4 helped Terence Tao discover a small bug in his recent paper

Attached: 1 image 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}...