### Abstract

We give a verified implementation of the Karatsuba Multiplication on Integers as well as verified runtime bounds. Integers are represented as LSBF (least significant bit first) boolean lists, on which the algorithm by Karatsuba is implemented. The running time of $O\left(n^{\log_2 3}\right)$ is verified using the Time Monad defined in Root-Balanced Trees by Nipkow.

### License

BSD License

### Topics

- Computer science/Algorithms
- Computer science/Algorithms/Mathematical

### Related publications

- https://mediatum.ub.tum.de/doc/1717658/1717658.pdf

### Session Karatsuba

- Karatsuba_Preliminaries
- Karatsuba_Sum_Lemmas
- Monoid_Sums
- Estimation_Method
- Time_Monad_Extended
- Main_TM
- Abstract_Representations
- Abstract_Representations_2
- Nat_LSBF
- Karatsuba_Runtime_Lemmas
- Nat_LSBF_TM
- Int_LSBF
- Karatsuba
- Karatsuba_TM
- Karatsuba_Code_Nat

### Depends on

- The Akra-Bazzi theorem and the Master theorem
- Expander Graphs
- Root-Balanced Tree

### Used by

- Schönhage-Strassen Multiplication

### Auto-related entries

- Schönhage-Strassen Multiplication

## Cite

×

Karatsuba-AFP

    @article{Karatsuba-AFP,
      author  = {Jakob Schulz and Emin Karayel},
      title   = {Karatsuba Multiplication on Integers},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Karatsuba.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest