This isn't about Terry Tao specifically, but proof assistants can help you manage a proof when it's gotten too big or complex to manage in your head without mak

This isn't about Terry Tao specifically, but proof assistants can help you manage a proof when it's gotten too big or complex to manage in your head without making mistakes. There was this project to use Lean to prove a theorem of Peter Scholze's (Scholze is a well-respected professor and a famous mathemtician). Apparently, it was so big and complex that he could barely keep it in his head, so after writing the proof, he and Kevin Buzzard formalized it with Lean. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm... Then, 6 months later, he was interviewed, where he talks about using Lean for proving his theorem: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... And the experiment was finished in 2022. Announcement: https://leanprover-community.github.io/blog/posts/lte-final/ https://leanprover-community.github.io/blog/posts/lte-final/