M mathstodon.xyz Lean4 helped Terence Tao discover a small bug in his recent paper 497 points gridentio 3 years ago 220 comments