I Vibed a Proof of Conway's Conjecture

Dan Abramov describes an AI-assisted effort that produced a machine-checked Lean proof of Conway’s refinement conjecture for omnific integers. The conjecture asserts that whenever ab = cd among omnific integers there exist e, f, g, h with a = ef, b = gh, c = eg, d = fh. Omnific integers are the “integer” subset of Conway’s surreal numbers, including ordinary integers and infinite ordinals like ω and combinations such as 2ω or ω^ω. Recent reductions in the literature translate the conjecture into a question about whether every irreducible element of K((ℝ^≤0)) with infinite support is prime; leveraging that reduction and formalizing the statement in Lean made automated checking possible. The formalization passed the Palomar registry’s mechanical checks and several Lean-fluent readers found the statement and approach plausible, though independent mathematical verification is still invited.

The writeup explains the workflow and software choices: initial sessions with Claude suggested the problem and produced grandiose, often incoherent drafts; ChatGPT served as a skeptical, constructive checker that produced smaller verifiable claims and helped locate robust ideas. Abramov converted papers to TeX, forked verification sessions, then ran a local Codex orchestration of agents (project manager, verifiers, searchers) to drive formalization and proof search, spending about a month and many tokens. The narrative emphasizes practical lessons about combining human oversight, multiple AI personalities, and mechanized proof tools to turn heuristic insight into a Lean formal proof.