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!

▲

adgjlsfhk1 2 hours ago | parent [-]

Have you considered looking at this in ram model rather than multi tape? it makes things a lot simpler

▲

jdb1729 2 hours ago | parent [-]

For one thing, the RAM model isn't fine-grained equivalent to MTTM (an example is https://en.wikipedia.org/wiki/Counting_sort which is linear-time on RAM but not MTTM). So, the result might not be the same. But also, Mathlib lacks a RAM machine implementation. So any proof would rest on a custom definition stack which would make it difficult to audit.

	▲	adgjlsfhk1 2 hours ago \| parent [-]
		yeah in ram models, this turn into O(n^1-kappa) , but otherwise the result is pretty similar (but you can drop the bit network part since matrix transposition is easy in RAM)