Fine-Grained Proof Complexity for Elementary Arithmetic in Extended Frege

We study the quantitative efficiency of propositional proofs and give quasi-linear-size Extended Frege proofs of basic laws of integer arithmetic. The construction uses a technique called index generalization and represents multiplication with an FFT-based algorithm.