Skip to content
Better HN
Top
New
Best
Ask
Show
Jobs
Search
⌘K
Running Lean at Scale
(opens in new tab)
(harmonic.fun)
67 points
eab-
2mo ago
6 comments
Share
Running Lean at Scale | Better HN
6 comments
default
newest
oldest
jarmitage
2mo 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
2mo 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
2mo 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
2mo ago
Lean4 with a mathlib project seems really slow has anyone else experienced that?
ncgl
2mo 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
2mo 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
j
/
k
navigate · click thread line to collapse