Terry Tao posted on Mastodon that he found a bug in a proof in one of his papers thanks to trying to formalize it in Lean. This is an excellent use case of Lean and tbh the only one tha . . . Read more