GoKawiilA 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:
It contains all real numbers (the numbers we use like 0, –5, 36.6, square root of 2…)
... continue reading