Grok is a surprisingly good automated theorem prover
By henryrobbins00 · 2026-07-22 · 1 points · 1 comments
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 accur…
Open the full discussion on BetterNews