4 ms·
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:
by adbachman 3y ago
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 https://mathstodon.xyz/@tao/111271244206606941
- omneity 3y agoThanks for adding the clarification. I thought this was more common knowledge. I will update my comment accordingly.