[英文] 數學家陶哲軒用程式輔助證明除錯

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}...