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!
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.
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)
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...
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 3 orders of magnitude above and below.
Except because it's some sort of a vibecoded atrocity, nothing happens if you try to toggle from "all" to "last 3 days", it only works if you change the value (e.g., to 2 or 4 days).
Stuff like that is really frustrating because it's not like we didn't have one zillion decent, human-tested graphing frameworks before.
I think it's basically an alignment problem. LLMs tend to think it's better to just do something small and bespoke than to just pull a mature library and use it correctly, which, to be clear, they are perfectly capable of doing.
And this is in part a reflection of our own bad preferences. This is what always annoyed me most about the left-pad Discourse a decade (oh god, a Decade™) ago; "why do you need a library for something so simple in the first place!?" people would scoff. And of course the answer is that even the reference class of left-pad-like problems includes a bunch of examples where the problem has bizarre and sticky edge cases you'd never consider, so in general, "just pop in a popular and well tested library" is actually a pretty good policy (assuming your package repository doesn't allow anything really silly like deleting entire packages and breaking everything downstream).
Of course charting is more obviously complicated, but again, it might seem fairly simple if all you're thinking about is one kind of chart in one style with limited settings. The difference is that for a human coder, "just whip up some chart code" is enough of a pain in the ass that they'll reach for a library by default, whereas a coding agent can just spit something out which mostly works in a few seconds.
All else equal, I'd rather have the richest possible functionality built into the language. At least I know that it will be updated and maintained in one place, and there's very little ambiguity about setup. You don't have to start picking apart the fact IN THIS PARTICULAR PROJECT, libfoo was imported by pasting it in the code base in 1977 before package management existed and globally namespaced, but libbar is a first-class citizen in the depency-injection system.
If you know you can just call bargraph($data), even if the stock bargraph library is boring, then people and LLMs will favour it.
I suspect they used an underpowered model, or did it a while back. I would be surprised to see 6.1 Sol or Astra produce those bugs, even one-shotting. Instead, I'd just expect it to have broader product issues rather than out and out bugs.
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.
@platypii and I have been pursuing Lean verification of improvements to kappa here: https://github.com/platypii/integer-mult-bounds-lean
Current status of the campaign: kappa >= 2^-14.38 proved unconditionally on Mathlib's TM2 machine. Contributions welcome!
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!
Have you considered looking at this in ram model rather than multi tape? it makes things a lot simpler
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.
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)
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 integer multiplication improvements generalize to DFT over prime-order finite fields, see: https://github.com/platypii/integer-mult-bounds-lean/blob/ma...
This might help, https://web.maths.unsw.edu.au/~davidharvey/research/subnlogn...
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...
See also https://bigospeedrun.com/integer-multiplication
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 3 orders of magnitude above and below.
To be fair it's a live graph, you can decrease the number of days and then the plot becomes more meaningful.
Except because it's some sort of a vibecoded atrocity, nothing happens if you try to toggle from "all" to "last 3 days", it only works if you change the value (e.g., to 2 or 4 days).
Stuff like that is really frustrating because it's not like we didn't have one zillion decent, human-tested graphing frameworks before.
I think it's basically an alignment problem. LLMs tend to think it's better to just do something small and bespoke than to just pull a mature library and use it correctly, which, to be clear, they are perfectly capable of doing.
And this is in part a reflection of our own bad preferences. This is what always annoyed me most about the left-pad Discourse a decade (oh god, a Decade™) ago; "why do you need a library for something so simple in the first place!?" people would scoff. And of course the answer is that even the reference class of left-pad-like problems includes a bunch of examples where the problem has bizarre and sticky edge cases you'd never consider, so in general, "just pop in a popular and well tested library" is actually a pretty good policy (assuming your package repository doesn't allow anything really silly like deleting entire packages and breaking everything downstream).
Of course charting is more obviously complicated, but again, it might seem fairly simple if all you're thinking about is one kind of chart in one style with limited settings. The difference is that for a human coder, "just whip up some chart code" is enough of a pain in the ass that they'll reach for a library by default, whereas a coding agent can just spit something out which mostly works in a few seconds.
Maybe the problem is libraries themselves.
All else equal, I'd rather have the richest possible functionality built into the language. At least I know that it will be updated and maintained in one place, and there's very little ambiguity about setup. You don't have to start picking apart the fact IN THIS PARTICULAR PROJECT, libfoo was imported by pasting it in the code base in 1977 before package management existed and globally namespaced, but libbar is a first-class citizen in the depency-injection system.
If you know you can just call bargraph($data), even if the stock bargraph library is boring, then people and LLMs will favour it.
All those mature charting packages are solidly inside the LLM’s training set, I’m a little surprised it can’t do a better job of reproducing them.
I suspect they used an underpowered model, or did it a while back. I would be surprised to see 6.1 Sol or Astra produce those bugs, even one-shotting. Instead, I'd just expect it to have broader product issues rather than out and out bugs.
Just because it can doesn't mean it will unless you tell it to. LLMs aren't magic do-what-I-mean beans.
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.
It is amazing to see how fast these bounds are moving.
I feel bound to say they’re bounding along boundlessly