Feasibility of Primality in Bounded Arithmetic

We prove the correctness of the AKS algorithm {AKS} within the bounded arithmetic theory Tᶜᵒᵘⁿᵗ₂ or, equivalently, the first-order consequence 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 show 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.