We are excited to see the top ranked pure mathematician feel comfortable using theorem provers in VS Code with GitHub Copilot to formally verify recent discoveries https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/

https://twitter.com/code/status/1732787495253766285