Dan Abramov (gaearon) claims a Lean proof of Conway's 1976 omnific integer conjecture, unverified by mathematicians
- Dan Abramov, known in the React community as gaearon, published a Lean proof of John Conway's 1976 conjecture that omnific integers have a refinement property, spending a month of free time and what he calls a boatload of tokens. The proof has not been independently verified by mathematicians.
- The conjecture states that if ab = cd for omnific integers a, b, c, d, then omnific integers e, f, g, h exist with a = ef, b = gh, c = eg and d = fh.
- The proof passed the mechanical checks of the Palomar registry (entry PALOMAR-2026-09-03-000002), and people familiar with both Lean and the field said the statement looks correct. Abramov invites a refutation.
- Claude picked the problem itself after Abramov asked which open question in surreal numbers pulled it most. Its answer tied Conway's conjecture to the L'Innocente-Mantova reduction, which asks whether every irreducible in K((R^<=0)) with infinite support is prime.
- Abramov calls himself a math noob and deliberately avoided understanding the substance. He framed the project as a test of whether he could pick an open problem and have a frontier model solve it, and notes the result depends on the Lean kernel having no bug.
Hacker News opinions
I got lost on day two. Two gaps, "between nothing and zero" and "between zero and nothing", and I'm officially too dumb for math.
That explanation is genuinely bad. A surreal number is a pair of sets of surreal numbers, built up in waves. "Nothing" just means the empty set. Go read On Numbers and Games, or have an LLM walk you through the Wikipedia page.
I think it's only that we have no notation for these numbers, so you invent names like -1 and 1. The labels don't matter, position does. The author even added a diagram to the post after people complained.
The part nobody explains is the rule for which number goes in each gap. From the examples he only averages the two neighbors, which would give you the rationals and never anything infinite or irrational.
You can define it cleanly: start with no numbers, then the empty set on both sides gives 0. Left numbers must be smaller than right numbers, and the value is the simplest number in between.
Someone please vibe-prove that ZFC is inconsistent.
Congrats. I figure in three months, once we all have communicating agent swarms, this kind of thing gets a lot easier.
The infinite monkey framing undersells it in the wrong direction. A finite number of LLMs with fixed weights cannot prove all theorems, because that would make the busy beaver sequence computable and the halting problem decidable. Prompting adds an information source from outside, which is what removes the limit.
Same argument applies to people though. Given infinite thinking time a finite number of humans solves all theorems. What exactly does AI have to do before people admit these systems are smart instead of calling it brute force?
The timing next to Gowers' post is wild. He argued problem-solving ability and conceptual understanding have come apart, and this guy ran the ultimate meta-experiment: 100% problem-solving, 0% understanding.
And the timing right after Gowers' post feels like a well-oiled marketing machine at work.