I vibed a proof of Conway's conjecture
Points and comments are a snapshot, not live.
A math noob used AI to produce a Lean proof of Conway's 50-year-old refinement conjecture.
Dan Abramov (gaearon) spent a month using Claude, ChatGPT, and Codex to obtain a Lean-formalized proof of Conway's refinement conjecture for omnific integers. The proof has passed the Palomar registry's mechanical checks and a few people familiar with Lean and the field say the statement seems correct, but it has not been independently verified by mathematicians. Abramov describes his workflow: initially one-shotting failed badly, producing AI-generated 'word salad'. He then set up a multi-agent system with roles (PM, Math, Red, Random, Lean) running in Codex, which produced a large TeX document and Lean code. He notes the proof may rely on a Lean kernel bug, but invites refutation.
What commenters are saying
The top comment expresses confusion about the surreal number explanation, with several commenters offering clarifications. One commenter explains the construction more explicitly: a surreal number is defined as a pair of sets of pre-existing surreals (L|R), starting from ∅|∅ = 0. Others note the explanation omits the precise rule for which number goes in each gap. A subthread discusses the potential for AI tutors that adapt to individual learning styles. One commenter suggests asking for analogies in a domain you already understand.