I’d like to nominate the graph there for some sort of crime, for using a log scale from 1e-55 to 1, where there is one result at 1e-55, one result at 1e-18, a million results at 1e-3, the omgwtfbbq threshold drawn at 1… and each result is drawn as a bubble that covers 6 orders of magnitude.
Eh, then it just shows relative change between results; in isolation, yes, not contextualising these results at all is better than misrepresenting them, but doing both is arguably worse than either, it kind of admits you know exactly what to avoid saying.
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!
Does anyone know if there's a simple way of understanding how exactly this speedup works? Standard O(N log N) multiplication uses frequency decomposition via FFT, iiuc; what might this construction look like?
The tldr is that you can turn a single fft into an n dimensional fft, into n 1d ffts and then share a very small amount of the work of the multiple ffts
"Apply the verified fresh-helper retiming to all 19 full native calls of #4440's p17 query-thinned complex controller. All 16 paid query shears, whole idle calls, main operators and the stronger BIT supplier are retained. "
I understand many of those words but apparently none of them within context...
12 comments
[ 2.9 ms ] story [ 22.9 ms ] threadCurrent status of the campaign: kappa >= 2^-14.38 proved unconditionally on Mathlib's TM2 machine. Contributions welcome!
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!
I understand many of those words but apparently none of them within context...