> Large language models (LLMs) are like prediction engines — when given a prompt, they generate a response by predicting what words are likely to come next. As a result, they’ve been extremely capable on language and creative tasks, but weaker in areas like reasoning and math. In order to help solve more complex problems with advanced reasoning and logic capabilities, relying solely on LLM output isn’t enough.

And yet I've heard AI folks argue that LLM's do reasoning. I think it still has a long way to go before we can use inference models, even highly sophisticated ones like LLMs, to predict the proof we would have written.

It will be a very good day when we can dispatch trivial theorems to such a program and expect it will use tactics and inference to prove it for us. In such cases I don't think we'd even care all that much how complicated a proof it generates.

Although I don't think they will get to the level where they will write proofs that we consider, beautiful, and explain the argument in an elegant way; we'll probably still need humans for that for a while.

Neat to read about small steps like this.