A few months ago, AI math results started making headlines. Naturally, I became curious whether I, a math noob, can find an open problem and have a frontier model solve it. It took an entire month of free time and a boatload of tokens, but I believe I've obtained a Lean proof of Conway's refinement conjecture, posed 50 years ago.

The conjecture claims that if ab = cd, there are integers e, f, g, h such that a = ef, b = gh, c = eg, and d = fh. My proof has not been independently verified by mathematicians. However, I have decent reasons to believe it is correct and genuinely invite a refutation.

The proof has passed mechanical checks from the Palomar registry, and people familiar with Lean and the field said the statement seems correct. So, assuming it doesn't rely on a kernel bug, it's likely legit. In this post, I'll describe my approach and things learned.

Choosing the Field I asked Claude to pick an open problem in surreal numbers. Surreal numbers are John Conway's invention, a number system containing all numbers great and small: all real numbers, ordinal numbers like infinitely large omega, and combinations like 75 + omega*3 + 1/omega. What is miraculous is that this rich system spawns from a single rule: spawn a new number in every gap between numbers already have.

Choosing the Problem Initially, I asked Claude for unsolved problems in the surreal numbers research program.