the missing context from the previous comment is that Tao used GitHub Copilot to... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		adbachman on Oct 27, 2023 \| parent \| context \| favorite \| on: Lean4 helped Terence Tao discover a small bug in h... 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 on Oct 27, 2023 [–]

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

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact