61 points | by eab- 11 hours ago ago
4 comments
This is part of the work that lead to Aristotle, the system that performed at Gold level at IMO: https://arxiv.org/abs/2510.01346
In case you want to try Aristotle, I asked Claude Code to make a plugin for it here https://github.com/afhverjuekki/claude-code-aristotle-plugin
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).
am i understanding it right that this is used to validate the output of llms? any other uses for distributed lean? genuinely curious
This is part of the work that lead to Aristotle, the system that performed at Gold level at IMO: https://arxiv.org/abs/2510.01346
In case you want to try Aristotle, I asked Claude Code to make a plugin for it here https://github.com/afhverjuekki/claude-code-aristotle-plugin
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).
am i understanding it right that this is used to validate the output of llms? any other uses for distributed lean? genuinely curious