> It would be good to have a formalised proof of the o(n log n) result, for example in Lean. As far as I can tell, one does not yet exist.
The result is fully formalized in Lean by @platypii and myself (on Mathlib's TM2 machine), with ongoing improvements to the exponent (currently at 1-2^-14.38): https://github.com/platypii/integer-mult-bounds-lean
> The new result does not directly imply new complexity bounds for polynomial multiplication over a fixed finite field, say multiplication in F2[x]. The state of the art for this problem is an algorithm that multiplies polynomials of degree n in time O(n log n 4^log*(n)) [HvdH19].
Note in this case the title says "O(n log n)", but the important part is this is "o(n log n)", not just "O(n log n)'. The former is a strict subset of the latter. We already knew how to multiply two n-bit integers in O(n log n) time, via the FFT.
Roughly speaking, O(n log n) means "grows no faster than k(n log n) for some k", whereas o(n log n) means grows strictly more slowly* than k(n log n) for all* choices of k.
Both define upper boundary, but big O can read like "the function is generally proportional to ___" and little o can read like "the function is never more than _____"
> I have not actually read the paper. In fact, there are three closely related papers [TC26a], [TC26b], [TC26c], and I have not read any of them. I tried, but soon gave up. The math(s) dump does not appear to be strong on exposition. Instead, I asked Fable to explain [TC26a] to me. Fable seems to understand the argument and thinks that it is correct.
Fable was able to help a human understand the paper though, so the situation is quite a bit better than if we just had a lean proof that was apparently correct but for which all attempts at explanation were "hallucinations". There doesn't seem to be an apparently obstacle to a human fully understanding the proof in several months of focused study.
Why not? If mathematicians in the field cannot understand the papers, but tools at our disposal can, why not use them? What is "unhealthy" about that? Just seems like it's the reality of the world now.
Honestly it is not that much different from the divine inspiration if you have ever experienced it.
I do not know how you view the world or walk through it but language in general is simply subject to interpretation to me, the arrangement of words for the sentence is inspiration in and of itself - though the majority of time it amounts to minimum jumps.
Awesome write up and intro by a fellow Sydney-sider, kept me hooked! As someone who's not a maths wizard, the technical details flew by my head but the prose allowing me to empathise deeply with those in the field was very enlightening. I never realised how big of a deal the maths dump was and how much it has shaken up the field. I guess we are all just trying to figure out this whole "intelligence on tap" thing together.
You don’t need to be a math wizard. Just upload the paper to an AI and ask, “Explain this like I’m five.” Then, with each follow-up prompt, increase the age and level of expertise you want it to assume.
> It would be good to have a formalised proof of the o(n log n) result, for example in Lean. As far as I can tell, one does not yet exist.
The result is fully formalized in Lean by @platypii and myself (on Mathlib's TM2 machine), with ongoing improvements to the exponent (currently at 1-2^-14.38): https://github.com/platypii/integer-mult-bounds-lean
Contributions are welcome!
> The new result does not directly imply new complexity bounds for polynomial multiplication over a fixed finite field, say multiplication in F2[x]. The state of the art for this problem is an algorithm that multiplies polynomials of degree n in time O(n log n 4^log*(n)) [HvdH19].
@platypii and I obtained a Lean proof of the same improvement for DFT over prime-order finite fields (yielding polynomial multiplication via the convolution theorem): https://github.com/platypii/integer-mult-bounds-lean/blob/ma...
> Executive summary (longer version) > The bottom line is that I think the claimed result is plausible. I have not actually read the paper.
Note in this case the title says "O(n log n)", but the important part is this is "o(n log n)", not just "O(n log n)'. The former is a strict subset of the latter. We already knew how to multiply two n-bit integers in O(n log n) time, via the FFT.
Roughly speaking, O(n log n) means "grows no faster than k(n log n) for some k", whereas o(n log n) means grows strictly more slowly* than k(n log n) for all* choices of k.
For those of us uninformed, what’s the difference between O and o?
Knuth originally defining them https://dl.acm.org/doi/10.1145/1008328.1008329
f(n) = O(g(n)) means as n increases, f(n)/g(n) must not grow beyond a constant
f(n) = o(g(n)) means as n increases, f(n)/g(n) must shrink
Nitpick:
s/must shrink/must eventually shrink, after finitely many n/
Equivalently, must go to zero in the limit.
depends on what you think shrink means. If you mean decreasing, that's false even eventually.
Big O basically drops constants
O(2n+1) = O(2n) = O(n)
o(2n+1) > o(2n) > o(n)
Both define upper boundary, but big O can read like "the function is generally proportional to ___" and little o can read like "the function is never more than _____"
that's not the convention I know... (from CLRS algorithms book).
Big O is sort of like <=. little o is sort of like <.
https://dl.acm.org/doi/10.1145/1008328.1008329
yes, GP is slightly off, but the idea of <= and < is accurate.
O(n) is: "there exists a K such that, for sufficiently large n, K*n is always larger".
o(n) is: "for every K, for sufficiently large n, K*n is always larger". (So o(2n+1) and o(2n) and o(n) are the same thing.)
If f is O(g) and o(h) then
And> Lim f/g -> C a constant.
This isn't quite correct. O(g) doesn't require the limit to exist.
Lmao! If someone is asking the difference between big and little o notation this is absolutely not the right way to clarify it.
If you were joking then maybe you got me
I do hope you can find and reattach your ass; that does sound painful.
Both are upper bounds. But small o is strictly smaller than upper bound. Big O is not greater than upper bound.
https://stackoverflow.com/questions/1364444/difference-betwe...
ty, fixed. (ahh, copy paste.)
> I have not actually read the paper. In fact, there are three closely related papers [TC26a], [TC26b], [TC26c], and I have not read any of them. I tried, but soon gave up. The math(s) dump does not appear to be strong on exposition. Instead, I asked Fable to explain [TC26a] to me. Fable seems to understand the argument and thinks that it is correct.
this does not feel like a healthy place to be
Fable was able to help a human understand the paper though, so the situation is quite a bit better than if we just had a lean proof that was apparently correct but for which all attempts at explanation were "hallucinations". There doesn't seem to be an apparently obstacle to a human fully understanding the proof in several months of focused study.
Why not? If mathematicians in the field cannot understand the papers, but tools at our disposal can, why not use them? What is "unhealthy" about that? Just seems like it's the reality of the world now.
Fable is the "gadget" of language ELI5.
Honestly it is not that much different from the divine inspiration if you have ever experienced it.
I do not know how you view the world or walk through it but language in general is simply subject to interpretation to me, the arrangement of words for the sentence is inspiration in and of itself - though the majority of time it amounts to minimum jumps.
Awesome write up and intro by a fellow Sydney-sider, kept me hooked! As someone who's not a maths wizard, the technical details flew by my head but the prose allowing me to empathise deeply with those in the field was very enlightening. I never realised how big of a deal the maths dump was and how much it has shaken up the field. I guess we are all just trying to figure out this whole "intelligence on tap" thing together.
You don’t need to be a math wizard. Just upload the paper to an AI and ask, “Explain this like I’m five.” Then, with each follow-up prompt, increase the age and level of expertise you want it to assume.
That algorithm won't converge anytime soon. A pre-conditioner (i.e. at least some apprentice wizardy) helps.
Really enjoy the writing style here.