[omneity]

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

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]

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

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

[passion__desire]

Not to beat the point: LLMs are compiler for english (natural) language.