I Vibed a Proof of Conway's Conjecture

A 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.