4 ms·
That one of the brightest minds of our generation is able to increase his bandwidth with the combination of LLMs and automated proofs makes me super bullish on
by omneity 3y ago
That one of the brightest minds of our generation is able to increase his bandwidth with the combination of LLMs and automated proofs makes me super bullish on this tech combo in the future!
It starts with bug-fixing, then supports verification, until it starts propelling new discoveries and push the envelope.
We need a term when a dynamic like Moore's Law "infects" a field that had no such compounding properties before.
EDIT:
There's additional context that Terence Tao is using Copilot to help him learn Lean. As shared by adbachman: https://mathstodon.xyz/@tao/111271244206606941 https://mathstodon.xyz/@tao/111271244206606941
Could Terence have done it without Copilot? Sure, but like many of us he might not have initiated it due to the friction of adopting a new tool. I think LLM tech has great potential for this "bicycle for the mind" kind of scenarios.
- aylmao 3y agoLean 4 is a theorem prover, and has nothing to do with LLMs as far as I know though.
- aylmao 3y agoLean 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.
- passion__desire 3y agoNot to beat the point: LLMs are compiler for english (natural) language.