Tau-prover is an agentic theorem proving system built as part of our work in formal verification. It is optimized for proving machine code, but the same machinery applies to mathematics, so we put it to the test on the hardest benchmark we know of.
The Lean-Eval leaderboard measures performance at solving research-level mathematics problems, such as Fermat's Last Theorem, in Lean 4, a coding language used for theorem proving.
As of July 13, 2026, Tau-prover v1 has solved 103 of these problems. That places it third in the world, surpassing all frontier models, including GPT 5.6 and Claude Fable 5, with unparalleled compute efficiency.
The count will move. Problems are submitted continuously and several remain open, so the number above is a snapshot, not a final score.
We were delighted by the result.