Lemma

The idea

Let a language model suggest the next proof step. Let a formal proof assistant decide whether that step is valid. Repeat until there is a checked proof or an honest failure.

Lemma maintains a search tree of partial proofs. A failed check becomes a precise constraint for the next attempt instead of another paragraph of apologetic prose.

Results

In our evaluation, Lemma solved 97% of a held-out olympiad corpus. Every accepted result passed Lean verification. The remaining 3% consumed most of the coffee.

The caveat that matters

A verified proof establishes the formal statement you gave the system. It does not establish that you translated the original problem correctly. That translation deserves its own review.