Lean is highly useful for filtering large sets of candidate proofs generated by an LLM, potentially millions, to identify plausible or correct proofs.

“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.”