M mathstodon.xyz Lean4 helped Terence Tao discover a minor error in a recent PFR conjecture paper 2 points gridentio 2 years ago 2 comments