Retrieved article excerpt
Open article · Retrieved 2026-09-18T15:23:01.554795+00:00
# How I Vibed a Proof of Conway’s Conjecture
September 18, 2026
[Pay what you like](https://ko-fi.com/gaearon)
A few months ago, AI math results started making headlines. [“Do a breakthrough”](https://www.theargumentmag.com/p/computer-do-a-breakthrough-no-mistakes) became a Twitter meme. Naturally, I became curious whether I, too, a [math noob](https://github.com/gaearon/analysis-solutions), 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](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/#how-many-tokens) of tokens, but I believe I’ve obtained a Lean [proof](https://github.com/gaearon/conway-refinement) of this conjecture posed by John Conway 50 years ago:
Conjecture: Omnific integers have a refinement property: if ab = cd for omnific integers, then there are further integers e, f, g, h with a = ef, b = gh, c = eg, d = fh.
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](https://github.com/gaearon/conway-refinement#why-i-think-its-correct) to believe the proof is correct, and I genuinely invite a refutation.
The proof has passed the mechanical checks [from the Palomar registry](https://palomar-registry.org/entry?id=PALOMAR-2026-09-03-000002&version=1), and a few people familiar with both Lean and the field said that [the statement](https://github.com/gaearon/conway-refinement/blob/264445c93b78554c408e99e4e7f663693b4e91ab/ConwayRefinement/Standalone/Mathlib/InlineConwayRefinement.lean#L246-L257) 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.
---
## [#First Day](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/#first-day)
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.
### [#Choosing the Field](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/#choosing-the-field)
I asked Claude to pick an open problem in the field of [surreal numbers](https://www.scientificamerican.com/article/surreal-numbers-are-a-real-thing-heres-how-to-make-them/). 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:
- It contains all [*real*](https://en.wikipedia.org/wiki/Real_number) numbers (the numbers we use like 0, –5, 36.6, square root of 2…)
- It also contains all [*ordinal*](https://en.wikipedia.org/wiki/Ordinal_number) numbers (the infinitely large ω, the ω + 1 that comes after it, the ω \* 2, and even ω \* ω, at some point even the impossibly large ω^ω…)
- Finally, it contains all kinds of unholy combinations of them, like 75 + ω\*3 + 1/ω.
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.
Think about it:
1. On the first day, the gap is “between nothing and nothing”. Zero is born.
2. 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.
3. 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.
The surreal number tree
*(Illustration by Joel David Hamkins. Go [read his posts](https://www.infinitelymore.xyz/p/surreal-numbers) and [buy his book!](https://jdh.hamkins.org/the-book-of-infinity/))*
Suppose we *actually* do this forever (an infinity of steps), then forevermore (an infinity of infinities of steps), and so ever on and on, never stopping birthing new numbers. It turns out that the binary tree based on this single rule will eventually give us every real, every ordinal, and more, with consistent arithmetic on them.
Surreal numbers are beautiful, and that’s why I asked Claude to work in that area.
### [#Choosing the Problem](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/#choosing-the-problem)
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 replied:
> **Claude:** I pick Conway’s arithmetic. Specifically, the question the [L’Innocente–Mantova machinery](https://doi.org/10.1016/j.aim.2024.109513) 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](https://en.wikipedia.org/wiki/On_Numbers_and_Games)’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.](https://claude.ai/share/b224fb11-8931-4d06-ad32-cdd06ce4d874) 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.
### [#The Problem Statement](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/#the-problem-statement)
While you’re probably here to learn more about my Lean/AI workflow, I’ll briefly explain the conjecture itself, since you already know enough to understand it.
In short, *omnific integers* are the integer part of the surreal number tree. So they include all regular integers like 3, –5, and so on, but also the weirder numbers like the infinitely large ω, 2ω, ω \* ω, ω^ω, –ω/7 (yes, that’s a “whole” number), etc. If you look at the binary tree above, you’ll notice that the omnific integers are the surreal numbers that you get if you *only ever go left* (e.g. –5, –ω–1), or *only ever go right* (e.g. 3, 2ω), or *only ever change directions exactly after infinite jumps* (e.g. ω/2).
Now, the conjecture.
Conway suggested that if `ab = cd`, we can break `a` and `b` into pieces, and `c` and `d` will turn out to be the same pieces recombined. With regular integers, we take this for granted: take 210 = 10 × 21. We can break 10 down as 2 × 5 and 21 as 3 × 7, then reshuffle them into 2 × 3 = 6 and 5 × 7 = 35. The product is still 6 × 35 = 210. So when we see some equality like 10 × 21 = 6 × 35, we know that under the hood there’s actually four numbers being reshuffled: (2 × 5) × (3 × 7) = (2 × 3) × (5 × 7).
However, when you deal with infinities, things don’t always turn out as we expect. So the conjecture means Conway thought omnific integers had, in a sense, enough “structure” to keep this “nice” property of integers. And conveniently, the recent advances have reduced the conjecture to proving a property of a certain kind of infinite series, and Claude thought we might now have enough to finish it off.
But can we actually do that solely with AI?
I’d say yes, and no, and yes.
---
## [#First Week](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/#first-week)
### [#One-Shotting, And Failing Badly At It](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/#one-shotting-and-failing-badly-at-it)
My first attempts involved plainly telling the AI to solve the conjecture (or to find a counterexample, according to its initial suggestion). I asked Claude which papers it wants to read, converted those papers to TeX so that the model doesn’t need to repeatedly decode PDFs, and told it to pursue its chosen approach, for example:
> **Me:** hunting for counterexample sounds good. don’t hesitate to burn all my tokens on this. if you have to take weeks, that’s ok — do a breakthrough and find a structured counterexample. do not rest until you’ve found it, and don’t give up. if you stay focused and think hard and smart enough, i know that you can find it. game? i attached some stuff you might find helpful!
This didn’t work well. Although some ideas from these sessions might have ended up being relevant to the final proof, most output at this stage seemed to be word salad that Claude invented to justify its work and make it sound impressive.
Here is a typical example:
> **Claude:** The stage-1 obstruction of C\* is not rigid. With designed resonance — arithmetic-progression offsets making the window equations honest Toeplitz systems, which are exactly the graded convolution operators the formalism predicted — there is a strictly positive space of frontier data simultaneously compatible with both b and d, for coprime pairs, beyond anything divisibility can explain. And the control column confirms the resonance-necessity conjecture empirically: break the skeleton alignment and the joint kernel dies at the constrained window, exactly as the transversality heuristic predicted. So the specific fear built up by five closed doors — that Pitteloud-descended rigidity would propagate stage-wise and choke the correction system at birth — is answered: at stage 1, it does not. The den has air in it. This is the first pro-C\* evidence the hunt has produced, and it comes with a clean structural reading: rigidity governs exact and finite configurations; the window systems, which are the native habitat of the transfinite construction, have generic slack of small but nonzero dimension. Drift fuel exists.
I thought this sounded like bad science fiction. It was using Claude’s unbearable metalanguage, gave cutesy names to some intermediate results without concretely justifying them, and kept being extremely dramatic. Of course I couldn’t verify its claims, but worse, it didn’t seem coherent enough to pass to a real mathematician for review. So it seemed like a dead end, and I had to look for a different approach.
### [#Restarting with the Skeptic](https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/#restarting-with-the-skeptic)
I got tired of Claudeisms, so I wanted to give ChatGPT a try; Sol in particular.
I’ve started my ChatGPT sessions by giving it the related papers *and* the output from the previous Claude sessions, with an explicit note that Claude’s “paper” is AI-generated, and I wanted to get ChatGPT’s opinion whether it is bullshit or not.
ChatGPT would say it’s mostly bullshit, pointing to the made-up terminology, dramatic claims, trivial results dressed up in fancy language, incorrect inferences, and other defects. While I had no way to judge if ChatGPT’s criticism is true (since I