Theorem proving isn’t just about getting to QED — it’s about the thousands of tiny, tactical decisions that get you there. A new system called GamePad, built by researchers Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever, treats those decisions as a machine learning problem. They’ve essentially turned the Coq proof assistant into a training environment, capturing the step-by-step human moves that lead to a completed proof.
Coq works differently than the kind of automated solvers most AI researchers have played with. Users don’t just state a theorem and wait. They guide the system through a series of tactics, each one transforming the proof goal into something slightly simpler. That interactive style leaves a rich trail of data — exactly what you need if you want to train a model to predict what a human would do next.
The team zeroed in on two tasks. First, position evaluation: given where you are in a proof, how many steps are left? It’s like a chess engine estimating how many moves to checkmate. Second, tactic prediction: what’s the right move right now? They tested this on a couple of fronts, including a simple algebraic rewrite problem and something far more ambitious — baseline models trained on a formalization of the Feit-Thompson theorem, a landmark result in group theory whose original proof ran hundreds of pages.
That last choice is a signal. You don’t tackle the formalization of the odd order theorem unless you’re serious about stress-testing your approach on genuine mathematical depth. The paper doesn’t claim to have automated deep theorem proving overnight. Instead, it’s building the scaffolding: a way to capture human proof strategies and see if machines can learn them. The question hanging in the air is whether a model that learns to mimic tactical choices can ever learn the strategic intuition behind why those tactics were chosen in the first place.
