Running Lean at Scale

2 comments

• 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
• 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).