In case you want to try Aristotle, I asked Claude Code to make a plugin for it here <a href="https://github.com/afhverjuekki/claude-code-aristotle-plugin" rel="nofollow">https://github.com/afhverjuekki/claude-code-aristotle-plugin</a>
This is part of the work that lead to Aristotle, the system that performed at Gold level at IMO: <a href="https://arxiv.org/abs/2510.01346" rel="nofollow">https://arxiv.org/abs/2510.01346</a>
Very interesting. Do I get this right, running 500000 instances for 1 hour can be done for about $5000, or are there many hidden costs? (500000 * $0.01).
Lean4 with a mathlib project seems really slow has anyone else experienced that?
am i understanding it right that this is used to validate the output of llms? any other uses for distributed lean? genuinely curious