I Vibe-Coded a Lean Proof of Conway's 50-Year-Old Conjecture
I Vibed a Proof of Conway's Conjecture
Dan Abramov spent a month and a boatload of tokens having AI models attack Conway's refinement conjecture about omnific integers. Claude produced grandiose word salad; ChatGPT, asked to be skeptical, ground out small verifiable claims. The result is a Lean proof that passed the Palomar registry's mechanical checks but has not been independently verified by mathematicians. He invites refutation.
I thought the idea of "solving" a math problem without understanding its substance is rather absurd, which of course made it all the more appealing.