Is there an associated machine-checked proof of this?

We're in full vibe-code mode at work, so I understand both how powerful frontier models can be and how often they can over-confidently state subtly (or not so subtly) wrong things, even when you're taking great efforts to try to keep that from happening.

So without a Lean development or extensive human verification, I guess I'm a little bit skeptical, and even sort of hoping this is wrong - not just because of my not so positive feelings about AI, but by my disposition towards beauty in math. n log n is an awful lot nicer than what we have here.

Agree 100% on wanting machinr verification of AI generated math.

But in regards to beauty, i feel like multiplication already has a lot of non beautiful exponents. Best known matrix multiply is O(n^2.371). For integer factorization, the inverse of this problem, general number field sieve is a crazy subexponential.

If factorization is just barely subexponential, is it really that surprising that multiplication is just barely sub n lg n ?

We can just wait for whomever they stole THIS proof from to come forward with threatening emails sent by OpenAI.