1
Grok is a surprisingly good automated theorem prover
Grok在自动化定理证明中展现惊人性价比，准确率媲美Claude Code和Codex，速度更快、成本更低
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 …