The speaker thinks Lean is useful for exploring many candidate proofs because it can identify which candidates are plausible or correct.

“I think it's also extremely useful for exploring a wide variety of possible proofs. I mean, that's kind of the value of an LLM, that it can output, you know, millions of potential proofs, but you need to then quickly sort among them to the ones that are plausible or correct.”

“Lean can tell you which ones those are. Uh, at the same time, right, the expressive power of the models is getting so much better that you don't need everything to be outputted in Lean code to verify its correctness.”