A new search algorithm asks AI theorem provers to care about proof quality, not just whether a proof works.
Researchers built LEVER, a search method that scores partial proofs as it builds them, rather than cleaning up a finished proof afterward. It maps out possible proof paths as a branching graph and blends real progress with predictions about unsolved steps, so cost, length, and topical focus all factor into the search itself. Lean's own proof checker still verifies every result, so nothing gets through unverified. On PutnamBench, a set of Putnam competition problems formalized in Lean 4, LEVER cost 34% less than a strong single-conversation AI agent while pushing the solve rate from 80% to 96% under the same budget.
That's the headline, but the more interesting bit is the tunability: LEVER also trims how far proofs wander from their actual topic better than editing a finished proof afterward does, and it does so more cheaply and consistently. Users can dial the tradeoff between a cheaper proof and a more elegant one, which matters for teams building formally verified software where ugly-but-correct proofs pile up maintenance debt.
Still, the results so far come from one benchmark of competition math problems, not the sprawling, messy proofs that show up in real formal verification projects.