Yea it's been fun! Everyone pretty much assumed n log n was the actual limit for integer multiplication. So the OpenAI result was surprising!

But of the 722 proofs openai released, integer multiplication did NOT come with a lean proof. So I wanted to see if the result was real, or maybe was a flaw in the proof. So I created the repo, and started burning tokens. It was not easy even with AI! It took a couple days laying the ground work. A huge part of the challenge was keeping the proof checking fast. It took ~8 hours for lean to check the first version of the proof. I fought to get it back down to ~20 minutes. Then huge credit to @jdb1729 for joining the effort and actually completing the proof across the finish line! The theorem was true!

Once we proved the initial openai bound of 2^-182, we've been working on integrating improvements to the bound, and we're now up to K = 2^-14. Continuing to work on it, community contributions welcome!