Machine-assisted theorem proving

The basic setup has two parts. A proof assistant (such as Lean) holds a goal, the statement still to be proved. A model proposes a tactic (a proof step). The assistant applies it, and either reports an error or returns the new, smaller goals. The model then proposes the next step, and so on until no goals remain. Because the assistant checks every step, an incorrect proposal cannot slip into a final proof.

This is a search problem. At each state there are many possible next steps, and a proof may need dozens or hundreds of them in the right order. Systems typically combine a language model, which suggests promising tactics, with a search procedure (for example best-first search or a tree search) that explores several branches and prunes the dead ends. Some systems are also trained with reinforcement learning: they attempt problems, receive a reward when the checker accepts a proof, and improve from that signal. Others work in the whole-proof style, where the model writes a complete proof at once and the checker accepts or rejects it.

A useful consequence of formal checking is that data can be generated at scale: any proof the checker accepts is a new, verified training example.

There are three open problems the entry highlights.

1. Autoformalization. Most mathematics is written in informal language. To use a proof assistant, a statement must first be translated into formal syntax. A translation that is slightly wrong (too strong, too weak, or about a different object) produces a verified but meaningless result. Checking that a formal statement matches the intent is mostly a human task today.
2. Long-horizon planning. Competition problems may need a few clever ideas; research papers need chains of lemmas, new definitions and organisation across many pages. Current systems struggle to decompose a large goal into the right sub-goals.
3. Clean benchmarks. If problems or their solutions appear in the training data, a high score may reflect memory rather than reasoning. Constructing new, unseen test problems is itself a research task.

The field is also tied to the Lean library Mathlib, since the model needs a large store of known lemmas to apply. Progress in AI proving therefore depends partly on progress in formalization.