[aylmao]

Lean 4 is a programming language and theorem prover, and has nothing to do with LLMs as far as I know though.

[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.