Running Lean at Scale 2 days ago (harmonic.fun) 6 comments eab- Reply Add to library jarmitage 2 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 2 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 2 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). ncgl 1 day 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 1 day 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 whattheheckheck 1 day ago Lean4 with a mathlib project seems really slow has anyone else experienced that?
jarmitage 2 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 2 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 2 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).
ncgl 1 day 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 1 day 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 1 day 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
whattheheckheck 1 day ago Lean4 with a mathlib project seems really slow has anyone else experienced that?
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).
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
Lean4 with a mathlib project seems really slow has anyone else experienced that?