Comment on Grok is a surprisingly good automated theorem proverComments−henryrobbins00OP1moSome additional details about these results that didn't make it into the main post:- The OpenATP "standard provers" were used; see docs [5] for model / harness configuration details- Time and cost are function of effort level, which may lead to unfair comparison across provers- FATE-X excludes task 10 since claude and grok hit session limits- FATE-X excludes leanstral and aristotle due to temporary endpoint failures- Deepseek's FATE-X accuracy is corrected from 2 to 3 due to verifier bug (now fixed)- 2 FATE-X deepseek misses are sorry-free, but rely on native_decide- Claude's FATE-X miss is due to a failed delegation to a background subagent- All costs come from underlying CLI, except codex which uses pricing table
Comments
Some additional details about these results that didn't make it into the main post:
- The OpenATP "standard provers" were used; see docs [5] for model / harness configuration details
- Time and cost are function of effort level, which may lead to unfair comparison across provers
- FATE-X excludes task 10 since claude and grok hit session limits
- FATE-X excludes leanstral and aristotle due to temporary endpoint failures
- Deepseek's FATE-X accuracy is corrected from 2 to 3 due to verifier bug (now fixed)
- 2 FATE-X deepseek misses are sorry-free, but rely on native_decide
- Claude's FATE-X miss is due to a failed delegation to a background subagent
- All costs come from underlying CLI, except codex which uses pricing table