Feasibility of primality in bounded arithmetic

Abstract We prove the correctness of the AKS algorithm [1] within the bounded arithmetic theory $T^{\text {count}}_2$ or, equivalently, the first-order consequences of the theory $\text {VTC}^0$ expanded by the smash function, which we denote by $\text {VTC}^0_2$ . Our approach initially demonstrates the correctness within the theory $S^1_2 + \mathrm {iWPHP}$ augmented by two algebraic axioms and then shows that they are provable in $\text {VTC}^0_2$ . The two axioms are: a generalized version of Fermat’s Little Theorem and an axiom adding a new function symbol which injectively maps roots of polynomials over a definable finite field to numbers bounded by the degree of the given polynomial. To obtain our main result, we also give new formalizations of parts of number theory and algebra: • In $\mathrm {PV}_1$ : We formalize Legendre’s Formula on the prime factorization of $n!$ , key properties of the Combinatorial Number System and the existence of cyclotomic polynomials over the finite fields $\mathbb {Z}/p$ . • In $S^1_2$ : We prove the inequality $\text {lcm}(1,\dots , 2n) \geq 2^n$ . • In $\text {VTC}^0$ : We verify the correctness of the Kung–Sieveking algorithm for polynomial division.