platypii/integer-mult-bounds-lean
View on GitHub ↗ ★ 28 Lean
Lean 4 formalization (work in progress) of O(n log n · log^(-ε) n) integer multiplication on a multitape Turing machine
4 mentions on Hacker News by 1 person: 0 stories, 4 comments · first 2026-10-22 · latest 2026-10-22
20082026
-
…(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!
comment by jdb1729 · 2026-10-22 · in The recently proposed o(n log n) integer multiplication algorithm [pdf] -
…over prime-order finite fields (yielding polynomial multiplication via the convolution theorem): https://github.com/platypii/integer-mult-bounds-lean/blob/ma...
comment by jdb1729 · 2026-10-22 · in The recently proposed o(n log n) integer multiplication algorithm [pdf] -
The integer multiplication improvements generalize to DFT over prime-order finite fields, see: https://github.com/platypii/integer-mult-bounds-lean/blob/ma...
comment by jdb1729 · 2026-10-22 · in Κ = 0.003 for integer multiplication crossed -
@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.…
comment by jdb1729 · 2026-10-22 · in Κ = 0.003 for integer multiplication crossed