Hacker News
I Vibed a Proof of Conway's Conjecture
The author claims to have produced a Lean proof of Conway’s refinement conjecture, which states that for omnific integers, if \(ab=cd\) then there exist integers \(e,f,g,h\) with \(a=ef\), \(b=gh\), \(c=eg\), and \(d=fh\). The proof passed mechanical checks in the Palomar registry and received informal confirmation from experts familiar with Lean and surreal numbers. The author invites independent verification and refutation of the result.