Terence Tao: Formalizing a proof in Lean using GitHub Copilot and canonical