Comment by Someone

_If_ you have formalized a provable theorem in Lean, a simple bread-first search can prove it. It will take lots (and lots, and lots, and lots…) of time, though (https://en.wikipedia.org/wiki/General_Problem_Solver).

LLMs can do smarter searches, and will likely find proofs for most of them, but are not guaranteed to find a proof.