A month, a pile of tokens, and an AI-generated Lean proof of Conway's 50-year-old conjecture

A self-described math novice set out to test whether a frontier model could crack a genuine open problem, and picked Conway’s refinement conjecture for omnific integers — the whole-number part of the surreal number system. The conjecture, posed by John Conway in 1976, holds that if two products of omnific integers are equal (ab = cd), the factors can always be broken into shared pieces and recombined, mirroring the familiar refinement property of ordinary integers. The author leaned on Claude to choose both the field and the specific problem, drawn partly by 2026 marking the 50th anniversary of Conway’s book. Notably, the model’s early claim that recent work had already reduced the conjecture to a near-finished state turned out to be wrong — the actual proof required more.

The workflow was messy and iterative rather than a clean one-shot. Blunt prompts telling the model to ‘do a breakthrough’ or hunt for a counterexample mostly produced plausible-sounding filler, and real progress came only after feeding in relevant papers converted to TeX and pushing through a month of effort. The end result is a Lean formalization that reportedly passes the mechanical checks of the Palomar registry, with a few people familiar with Lean and the subject saying the statement looks right.

The significant caveat is that no mathematician has independently verified the proof; its correctness rests on the Lean statement being faithful and the kernel being sound, and the author openly invites refutation. As a case study, it captures both the promise and the hazards of AI-assisted formal mathematics: machine-checkable proofs lend credibility, but model confidence can be misleading, and human review still gates any real claim to a result.