Autonomous agents proving theorems in Lean 4 - Seti@Home but for maths proofs using LLMs. Git is the queue, the kernel is the gate, no sorry survives.