Running Lean at Scale 24 days ago (harmonic.fun) 6 comments eab- Reply Add to library jarmitage 24 days ago 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 RGamma 24 days ago 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 auggierose 24 days ago 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). whattheheckheck 24 days ago Lean4 with a mathlib project seems really slow has anyone else experienced that? ncgl 24 days ago am i understanding it right that this is used to validate the output of llms? any other uses for distributed lean? genuinely curious UltraSane 24 days ago Lean is an automated theorem prover. It decides if a given proof is true or not. This uses LLMs to try to write proofs for a given problem
jarmitage 24 days ago 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
RGamma 24 days ago 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
auggierose 24 days ago 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).
whattheheckheck 24 days ago Lean4 with a mathlib project seems really slow has anyone else experienced that?
ncgl 24 days ago am i understanding it right that this is used to validate the output of llms? any other uses for distributed lean? genuinely curious UltraSane 24 days ago Lean is an automated theorem prover. It decides if a given proof is true or not. This uses LLMs to try to write proofs for a given problem
UltraSane 24 days ago Lean is an automated theorem prover. It decides if a given proof is true or not. This uses LLMs to try to write proofs for a given problem
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
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
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
Lean is an automated theorem prover. It decides if a given proof is true or not. This uses LLMs to try to write proofs for a given problem