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?
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.
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.
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.
Current status of the campaign: kappa >= 2^-14.38 proved unconditionally on Mathlib's TM2 machine. Contributions welcome!
Stuff like that is really frustrating because it's not like we didn't have one zillion decent, human-tested graphing frameworks before.