Auto Research: Integer multiplication below n log n

Is there any good writeup yet of intuitively where the speedup comes from? E.g. with fast fourier transform you can see that there's a lot of symmetry & recomputation in the Vandermonde matrix, so that's where the speed up comes from.

I don't understand anything. Are the contributions in Lean?

Did they start with OpenAI's Lean proof and continue work on that?

Does the Lean proof grow significantly, or are they also trying to keep the Lean proof short-ish?

Oh no! You want to get our tokens for free

Some more context

https://nitter.kareem.one/RohanArun/status/21093360158149592...

(Replace top-level with healthy instances or x.com as needed)