Κ = 0.003 for integer multiplication crossed(github.com)
26 pointsby aleph_minus_one3 hours ago4 comments
  • jdb172935 minutes ago
    @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!

    • platypii19 minutes ago
      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!

      • adgjlsfhk16 minutes ago
        Have you considered looking at this in ram model rather than multi tape? it makes things a lot simpler
  • joeldw35 minutes ago
    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?
  • readthenotes117 minutes ago
    "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...

  • aleph_minus_one3 hours ago
    See also https://bigospeedrun.com/integer-multiplication
    • fwlran hour ago
      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.
      • prezkan hour ago
        To be fair it's a live graph, you can decrease the number of days and then the plot becomes more meaningful.
        • pinevalean hour ago
          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.

        • fwlr34 minutes ago
          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.
    • ebiederman hour ago
      It is amazing to see how fast these bounds are moving.
      • shrican hour ago
        I feel bound to say they’re bounding along boundlessly