[adbachman]

the missing context from the previous comment is that Tao used GitHub Copilot to help with learning Lean.

He's been writing about it as he goes, most recently: https://mathstodon.xyz/@tao/111271244206606941

[omneity]

Thanks for adding the clarification. I thought this was more common knowledge. I will update my comment accordingly.