3 ms·
Lean 4 is a programming language and theorem prover, and has nothing to do with LLMs as far as I know though.
by aylmao 3y ago
Lean 4 is a programming language and theorem prover, and has nothing to do with LLMs as far as I know though.
- adbachman 3y agothe 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.