Grok is a surprisingly good automated theorem prover TL;DR: I'm working on a Python package called OpenATP [1] that provides a common interface to coding agents for automated theorem proving in Lean. In the latest release, I added support for Leanstral 1.5 [2,3], Grok, and Kimi Code [4]. I was surprised to find that Grok has accuracy competitive with Claude Code and Codex at faster wall-clock times and a fraction of the cost. See the rest of this post and the OpenATP docs [5] for more details. Automated theorem provers take formal statements (in a proof assistant like Lean) and attempt to synthesize a proof. Unsurprisingly, LLMs have become the dominant approach to this task. Many have fine-tuned LLMs specifically for theorem proving, like Mistral's Leanstral 1.5 model. However, a number of recent papers have shown that general-purpose frontier models in a coding harness are competitive with, and sometimes outperform, these specialized models [6,7]. In my own research, I've had a lot of success using Claude Code and Codex as automated theorem provers. As new models and harnesses have been released in the last few months, I've been curious how they would compare, both in accuracy and in time/cost. I ran into two main issues trying to run benchmarks: - I needed to bill against subscription plans to make it affordable. - Compiling Lean is RAM intensive and I needed a cheap way to run multiple isolated agents in parallel remotely. I created an open-source Python package called OpenATP [1] to solve both of these problems. OpenATP automatically forwards agent CLI credentials into a Docker container to bill against subscription plans and it offers a Modal backend to run multiple agents in parallel remotely (Modal offers $30/month in free compute). See the OpenATP docs [5] for all of the supported provers / harnesses and how to set up credentials for each. The most recent release of OpenATP added support for Leanstral 1.5, Grok, and Kimi Code. I ran some small benchmarks on a subset of the FATE-H and FATE-X datasets [8] to compare them. The Kimi Code subscription rate limits were too restrictive to include it in the benchmark. On FATE-H, Claude Code and Codex are the fastest at ~10 minutes per proof. They are also significantly more expensive. Aristotle [9] is free and achieves perfect accuracy in 2x the time. Leanstral 1.5 is also free and has similar time and accuracy to Aristotle (the one miss was due to 60 min timeout). DeepSeek is incredibly cheap, but is also the slowest. It's roughly 3x slower than Claude and hits 3 timeouts. In comes Grok! Grok achieves accuracy comparable to Claude Code and Codex, but at a fraction of the cost and the fastest wall-clock time. The difference on FATE-X, a more challenging dataset, is even more pronounced. Grok is ~50% faster and ~3x cheaper than Claude Code and Codex. On these more challenging problems, the cheapest provers really begin to struggle. DeepSeek was 4x slower than Grok and hit 4 timeouts. FATE-H --------------------------------- prover acc. time cost t/o --------------------------------- claude 10/10 9:50 $2.05 0 codex 9/10 10:00 $2.68 0 grok 10/10 8:46 $0.94 0 deepseek 7/10 28:21 $0.15 3 leanstral 9/10 23:00 free 1 aristotle 10/10 19:39 free 0 --------------------------------- FATE-X --------------------------------- prover acc. time cost t/o --------------------------------- claude 8/9 15:43 $3.60 0 codex 9/9 14:27 $3.70 0 grok 9/9 10:42 $1.31 0 deepseek 3/9 41:48 $0.21 4 --------------------------------- [1] https://github.com/henryrobbins/open-atp [2] https://news.ycombinator.com/item?id=48780801 [3] https://mistral.ai/news/leanstral-1-5/ [4] https://news.ycombinator.com/item?id=48935342 [5] https://open-atp.henryrobbins.com [6] https://arxiv.org/abs/2601.14027 [7] https://arxiv.org/abs/2602.24273 [8] https://github.com/frenzymath/FATE [9] https://aristotle.harmonic.fun |