platypii / integer-mult-bounds-lean

git clone https://github.com/platypii/integer-mult-bounds-lean.git

Lean 4 formalization (work in progress) of O(n log n · log^(-ε) n) integer multiplication on a multitape Turing machine