Feasibility of Primality in Bounded Arithmetic

TL;DR

This work formalizes the correctness of the AKS primality test within weak, bounded-arithmetic theories by embedding the key number-theoretic and algebraic ingredients into $S^1_2+ ext{iWPHP}+ ext{RUB}+ ext{GFLT}$ and then carrying the result into $VTC^0_2$ (hence $T^{count}_2$). The approach hinges on two algebraic axioms—Generalized Fermat's Little Theorem and Root Upper Bound—to bridge primality reasoning with polynomial congruences, complemented by formalizations of Legendre’s formula, cyclotomic polynomials over finite fields, and efficient polynomial division (Kung–Sieveking) within bounded arithmetic. The paper proves that AKSPrime$(x)$ is equivalent to primality in these theories, and then shows that $VTC^0_2$ suffices to prove the necessary consequences of the auxiliary theories, securing AKSCorrect in the target bounded-arithmetic setting. The results illuminate the feasibility of proving nontrivial number-theoretic correctness results in weak theories and raise questions about the precise limits of $T_2$ and related systems for such endeavors, with potential implications for proof complexity and witnessing in bounded arithmetic.

Abstract

We prove the correctness of the AKS algorithm \cite{AKS} within the bounded arithmetic theory $T^{count}_2$ or, equivalently, the first-order consequence of the theory $VTC^0$ expanded by the smash function, which we denote by $VTC^0_2$. Our approach initially demonstrates the correctness within the theory $S^1_2 + iWPHP$ augmented by two algebraic axioms and then show that they are provable in $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: $\bullet$ In $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 $Z/p$. $\bullet$ In $S^1_2$: We prove the inequality $lcm(1,\dots, 2n) \geq 2^n$. $\bullet$ In $VTC^0$: We verify the correctness of the Kung--Sieveking algorithm for polynomial division.

Theorems & Definitions (168)

• Lemma 2.1: $\mathrm{PV}_1$, Euclid's algorithm
• Definition 2.2: Generalized Fermat's Little Theorem
• Theorem 2.3: jerabek2022iterated
• Lemma : A
• Lemma : B
• Lemma : C
• Lemma : D
• Definition : AKS
• Lemma : E
• Lemma : F