We prove the correctness of the AKS algorithm \cite{AKS} within the bounded arithmetic theory $T^{count}_2$ or, equivalently, the first-order consequences 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 $\mathbb{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.

翻译：我们在有界算术理论 $T^{count}_2$ 中证明了 AKS 算法 \cite{AKS} 的正确性，该理论等价于由 smash 函数扩展的理论 $VTC^0$ 的一阶推论，记作 $VTC^0_2$。我们的方法首先在 $S^1_2 + iWPHP$ 理论中，通过增加两条代数公理来证明其正确性，然后证明这两条公理在 $VTC^0_2$ 中是可证的。这两条公理是：费马小定理的一个推广版本，以及一条添加新函数符号的公理，该函数将可定义有限域上多项式的根单射地映射到由该多项式次数所限定的数。为了得到主要结果，我们还给出了数论和代数部分的新形式化：$\bullet$ 在 $PV_1$ 中：我们形式化了关于 $n!$ 的素数分解的勒让德公式、组合数系的关键性质以及有限域 $\mathbb{Z}/p$ 上分圆多项式的存在性。$\bullet$ 在 $S^1_2$ 中：我们证明了不等式 $lcm(1,\dots, 2n) \geq 2^n$。$\bullet$ 在 $VTC^0$ 中：我们验证了用于多项式除法的 Kung--Sieveking 算法的正确性。