FilterHN
new
ask
show
jobs
submit
FilterHN
show menu
Running Lean at Scale
45 points
by
eab-
2 hours ago
|
past
| 3 comments
|
harmonic.fun
|
HN
▲
jarmitage
1 minute 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
reply
▲
RGamma
1 hour 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
reply
▲
auggierose
1 hour 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).
reply