Feasibility of Primality in Bounded Arithmetic

We prove the correctness of the AKS algorithm [1] within the bounded arithmetic theory T ^count ₂ or, equivalently, the first-order consequences of the theory VTC ⁰ expanded by the smash function, which we denote by VTC ⁰ ₂. Our approach initially demonstrates the correctness within the theory S ¹ ₂ + iWPHP augmented by two algebraic axioms and then shows that they are provable in VTC ⁰ ₂. 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 PV ₁: 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 Z/p. In S ¹ ₂: We prove the inequality lcm(1,..., 2n) ≥ 2 ⁿ. In VTC ⁰: We verify the correctness of the Kung–Sieveking algorithm for polynomial division.