Another great paper from Google.

Shows general LLMs can solve formal math by planning proofs and checking each step. Raised general LLM performance from under 10% to 70%.

A general LLM failed badly when asked to write full formal proofs in 1 try， but became much stronger when it planned， split the work into smaller claims， reused past claims， and learned from Lean's feedback.

The paper shows the weakness was not just the model's math ability， but the way it was being used - the absence of structured interaction with a verifier.

The key idea is that the model does not try to write one giant perfect proof at once， because that usually fails on long and tricky problems.