GoKawiilIndependent researcher claims AI-assisted Lean proof of Conway's 50-year-old refinement conjecture
An amateur mathematician spent a month using a frontier AI model to attempt a formal Lean proof of John Conway's refinement conjecture about omnific integers in surreal number theory, a problem posed 50 years ago. The proof reportedly passed mechanical verification through the Palomar registry, and some Lean and field experts said the statement appears correct, though full independent mathematical verification is still pending.