[HN Gopher] Running Lean at Scale
       ___________________________________________________________________
        
       Running Lean at Scale
        
       Author : eab-
       Score  : 28 points
       Date   : 2026-01-13 21:50 UTC (1 hours ago)
        
 (HTM) web link (harmonic.fun)
 (TXT) w3m dump (harmonic.fun)
        
       | auggierose wrote:
       | 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).
        
       | RGamma wrote:
       | 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
        
       ___________________________________________________________________
       (page generated 2026-01-13 23:00 UTC)