henryrobbins00

This is super cool! I see you are using Aristotle as the automated theorem prover. I know Aristotle is free (for now at least), and it's hard to beat free... But, you still might be interested in a recent post of mine [1]! I'm working on an open-source Python package called OpenATP [2] to make it easy to run/benchmark different models and harnesses as automated theorem provers. I recently added support for Grok 4.5 and found it to be surprisingly good.

[1] https://news.ycombinator.com/item?id=49010310

[2] https://github.com/henryrobbins/open-atp

If you're excited about the relationship of Lean4 to LLMs/AI (like I am), you might find my recent post interesting [1].

TL;DR: I'm using automated theorem provers within my research on AI for automated algorithm design. To make it easier to run/benchmark different models/harnesses, I created an open-source Python package called OpenATP [2]. I recently added support to use Grok 4.5 in the OpenCode harness as a prover and found it to be surprisingly competitive with Claude Code and Codex at a fraction the cost and wall-clock time.

[1] https://news.ycombinator.com/item?id=49010310

[2] https://github.com/henryrobbins/open-atp

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

Earnest question: any recommendation to not come off this way in forums?

I created this tool for my own research and have found it really helpful to benchmark different automated theorem provers (my experience so far has been that Claude Code + Codex still out-perform Leanstral). My genuine aim is to share that usefulness with others, not self promote!

Try out Leanstral 1.5 on the latest version of OpenATP! OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It natively supports running provers locally in Docker or remotely in Modal sandboxes.

GitHub: https://github.com/henryrobbins/open-atp

Docs: https://open-atp.henryrobbins.com

Really? I get a 403 that I must enable Lab models on https://admin.mistral.ai/plateforme/privacy. When I try to do that, it gives "There was an error trying to update the Labs setting."

Do you have that Labs setting enabled? When I contacted support, they said "enabling Labs models isn't available for self-serve activation on standard individual accounts." Do you have a different type of account?

What a coincidence! I just released OpenATP earlier today. OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It includes support for Leanstral with Mistral’s Vibe harness. The previous production Leanstral model was deprecated on May 22nd. I will update the package to point to Leanstral 1.5 ASAP!

GitHub: https://github.com/henryrobbins/open-atp

Docs: https://open-atp.henryrobbins.com