Hobbyist claims month-long Claude collaboration yielded Lean proof of Conway's 1976 conjecture

What the author claims

A self-described "math noob" says they used a frontier AI model to produce a machine-checked Lean proof of a conjecture John Conway posed about the surreal numbers roughly fifty years ago. Writing on overreacted.io, in a post that reached Hacker News's front page, the author reports that the project took a month of free time and a considerable volume of tokens.

The result is not confirmed. The author states plainly that no mathematicians have independently verified the proof. What supports it, according to the post, is a pass on the mechanical checks run by the Palomar registry, plus informal assurance from a few people who know both Lean and the field that the formalized statement correctly captures the conjecture. Short of a bug in the Lean kernel itself, the author argues the proof is likely legitimate — and explicitly invites refutation.

The conjecture it targets

Surreal numbers, Conway's invention, form a number system containing all real numbers, all ordinal numbers (the infinitely large ω, ω + 1, ω × ω), and stranger mixtures such as 75 + 3ω + 1/ω. Their appeal, particularly to a programmer, is that this entire universe grows from a single rule: at every step, spawn a new number in every gap between the numbers you already have — including the gaps beyond everything on either side — and repeat forever.

Omnific integers are the integer-like part of that universe. They include ordinary integers such as 3 and –5, but also infinite "whole" numbers like ω, ω × ω and –ω/7.

Conway's refinement conjecture, from 1976, says these integers retain a property we take for granted with ordinary ones. With regular integers, 10 × 21 equals 6 × 35 because the factors can be reshuffled: 10 = 2 × 5 and 21 = 3 × 7 can be recombined as 2 × 3 = 6 and 5 × 7 = 35. Conway conjectured the same works for omnific integers: whenever ab = cd, there should exist e, f, g, h with a = ef, b = gh, c = eg and d = fh.

How the project unfolded

The author's method was to let the model steer. They first asked Claude to pick an open problem in the field of surreal numbers. After sessions of reading and narrowing, the model chose Conway's arithmetic — specifically, whether every irreducible with infinite support in a certain series ring, K((ℝ^≤0)), is prime. Recent work by L'Innocente and Mantova had reduced Conway's 1976 conjecture to exactly that question. Claude also noted that 2026 marks the fiftieth anniversary of Conway's book On Numbers and Games, which made the choice sentimentally appealing — though the author admits they could not confirm the model's claim that this was the last of Conway's own conjectures still standing.

One prerequisite was checked before committing: that the conjecture could be stated concisely in Lean. Without that, the author reasoned, even a correct proof would be impossible to get anyone to review.

The early attempts failed badly. The author asked Claude to either prove the conjecture or hunt for a structured counterexample, converted the relevant papers to TeX so the model would not have to repeatedly decode PDFs, and encouraged it to spend as much time and compute as needed. Most output at this stage, the author writes, was dense, impressive-sounding text invented to justify the work rather than real progress — although a few ideas from those sessions may have fed into the final argument. The result, in other words, came from a month of iteration rather than a single prompt.

Why it matters

This is a hands-on data point on frontier models as mathematical collaborators for people without domain expertise, arriving in a year when AI mathematics results have made headlines and "do a breakthrough" became a social media meme. The Lean formalization also changes what believing a proof requires: trust shifts away from reviewing the author toward reviewing whether the formal statement matches the conjecture and whether the checker itself is sound.

The limits are just as instructive. The proof awaits independent human verification, its correctness rests on the statement having been formalized faithfully and on the Lean kernel being bug-free, and naive one-shot prompting produced nothing usable. As a signal of where AI-assisted mathematics stands, the story is less about models solving open problems alone and more about what a determined amateur can now seriously attempt — with verification, not generation, remaining the bottleneck.