How I Vibed a Proof of Conway’s Conjecture — overreacted

A few months ago, AI math results started making headlines. “Do a breakthrough” became a Twitter meme. Naturally, I became curious whether I, too, a math noob, can find some open mathematical problem and then have a frontier model solve it.
It took me an entire month of my free time and a boatload of tokens, but I believe I’ve obtained a Lean proof of this conjecture posed by John Conway 50 years ago:
Conway’s refinement conjecture claims that omnific integers have a refinement property: if ab = cd, there are integers e, f, g, h with a = ef, b = gh, c = eg, d = fh.
My proof has not been independently verified by mathematicians. However, I have decent reasons to believe the proof is correct, and I genuinely invite a refutation.
The proof has passed the mechanical checks from the Palomar registry, and a few people familiar with both Lean and the field said that the statement seems correct. So, assuming my proof doesn’t rely on a Lean kernel bug, it’s likely to be legit too.
In this post, I’ll describe my approach, and some things I learned along the way.
I thought the idea of “solving” a math problem without understanding its substance is rather absurd, which of course made it all the more appealing.
However, I didn’t just want any result; I wanted something that pulls me.
I asked Claude to pick an open problem in the field of surreal numbers. In case you’re not aware, surreal numbers are John Conway’s invention—or a discovery?—of a previously unknown number system containing all numbers great and small:
What is particularly miraculous about surreal numbers (and why I suppose they might appeal to a programmer) is that this rich system spawns from a single rule.
Take all the numbers you have so far. Then, “spawn” a new number in every gap between the numbers you already have (crucially, “to the left of all” and “to the right of all” also count as “gaps”). Apply this step forevermore, and you’ll get surreal numbers.
On the first day, the gap is “between nothing and nothing”. Zero is born.
first, we cut between nothing and nothing. this gives us zeronothingnothingnothingnothing0
On the second day, there are two gaps: “between nothing and zero” and “between zero and nothing”. Two numbers spawn in those two gaps. Call them –1 and 1.
now we have two different places that can be cut. this gives us -1 and +1nothingnothingnothingnothing00–11
On the third day, there are four gaps: a gap “between nothing and –1”, a gap “between –1 and 0”, a gap “between 0 and 1”, and a gap “between 1 and nothing”. Put a number in each of those gaps and then give them names: –2, –1/2, 1/2, and 2.
now we have four places to make cuts. this gives us –2, –1/2, +1/2, +2nothingnothingnothingnothing00–1–1–1/21/2–2112
On the fourth day, we fill the eight gaps with –3 and 3 at the edges and –3/4, –3/2, 3/2, and 3/4 in the remaining gaps:
now we have eight places to make cuts. this gives us –3, –3/2, –3/4, –1/4, 1/4, 3/2, 3/2, 3nothingnothingnothingnothing00–1–1–1/2–1/2–3/4–3/23/43/2–1/41/41/21/2–2–2–311223
Suppose we actually do this forever (an infinity of “days”).
Jump to the “infinite-th” day (call it ω). With an infinite supply of the “already born” numbers, we’ll suddenly find infinitely many new “gaps” waiting to be filled that we couldn’t express before: “between [1, 2, 3, …] and nothing” (plus infinity?), “between nothing and […, –3, –2, –1]” (minus infinity?), “between 0 and [1, 1/2, 1/4, 1/8…]” (an infinitely small number?), “between [positive already born numbers whose squares are below 2] and [positive already born numbers whose squares are above 2]” (a square root of 2?), and so on. So, by this day, we have every real and we get our first infinitely large and small numbers (call them ω, –ω, 1/ω, and –1/ω).
Now suppose we keep on going then forevermore (through an infinity of infinities of days), and so ever on and on, never stopping birthing new numbers. It turns out that, if we go forever, the binary tree based on this single rule gives birth to every real, every ordinal, and more, with consistently definable arithmetic on them:
(Illustration by Joel David Hamkins. Go read his posts and buy his book!)
Surreal numbers are beautiful, and that’s why I asked Claude to work in that area.
Initially, I asked Claude:
Me: which unsolved problems in the Surreal Numbers research program pull you the most and why?
It suggested a number of things but noted some have had recent progress. I asked:
Me: get up to speed on the corners you want to know more about. follow your curiosity. you can look for older stuff too.
Then I further asked it to narrow down the choice to something concrete:
Me: what direction pulls you most? i want you to pick a problem to work on. be bold!
Claude: I pick Conway’s arithmetic. Specifically, the question the L’Innocente–Mantova machinery just sharpened to a point — is every irreducible in K((ℝ^≤0)) with infinite support prime? — which, by their reduction, is now exactly equivalent to Conway’s 1976 conjecture that any two factorizations of an omnific integer admit a common refinement. It’s the last of Conway’s own conjectures about his own numbers still standing, and 2026 is ONAG’s fiftieth birthday. That’s the problem I’d work on.
I still don’t know whether this really was Conway’s last standing conjecture about the surreal numbers (let me know either way!), but this year being his book’s 50th birthday convinced me to choose this problem for sentimental reasons.
Here is the full transcript from that session. My last question to that session was whether we have a chance of formalizing the Lean statement of the conjecture in a relatively concise way—without that, even if I found a proof, there’d be no way for me to convince somebody to look at it. Claude said it can be stated without much trouble in Lean, and that answer seemed right, so I decided to take on this project.
(Note: I didn’t know this at the time, but Claude’s claim about the problem having been perfectly reduced was wrong; actually prov