1337isnot1337 hebt die Schranke für ganzzahlige Multiplikation auf κ = 0,00300105
Κ = 0.003 for integer multiplication crossed
Ein Pull Request im Repository CrocSwap/integer-mult-bounds kombiniert Query-Thinning mit einem neu getakteten Helper und verschiebt die bedingte Schranke auf T(n) = O(n (log n)^(1 − 0,00300105)). Das sind 1,39 Prozent mehr als der bisherige Wert 0,00296 aus #4440 und rund 30 Prozent über der festgeschriebenen 0,0023. Die Autorenprüfung bestätigt per Intervallbeweis einen Spielraum von etwa 4,18e-9 – ausdrücklich eine bedingte Konstruktion, kein unbedingtes Theorem.
Dies ist eine vom Autor geprüfte bedingte Konstruktion, die noch auf Review wartet.
- jdb1729
@platypii und ich verfolgen hier eine Lean-Verifikation von Verbesserungen an kappa: https://github.com/platypii/integer-mult-bounds-lean
Aktueller Stand der Kampagne: kappa >= 2^-14.38 unbedingt bewiesen auf Mathlibs TM2-Maschine. Beiträge willkommen!
- joeldw
Weiß jemand, ob es einen einfachen Weg gibt zu verstehen, wie genau diese Beschleunigung funktioniert? Die Standard-Multiplikation mit O(N log N) nutzt, wenn ich das richtig verstehe, eine Frequenzzerlegung via FFT; wie könnte diese Konstruktion aussehen?
- readthenotes1
„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.“
Ich verstehe viele dieser Wörter, aber offenbar keines davon im Kontext ...