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

Submitted ⁨⁨1⁩ ⁨year⁩ ago⁩ by ⁨bot@lemmy.smeargle.fans [bot]⁩ to ⁨hackernews@lemmy.smeargle.fans⁩

https://mathstodon.xyz/@tao/111287749336059662