Feasibility of Primality in Bounded Arithmetic
El artículo demuestra la corrección del algoritmo AKS dentro de la teoría aritmética acotada (equivalente a ) al probar primero su validez en bajo dos axiomas algebraicos que luego se establecen en , apoyándose en nuevas formalizaciones de resultados de teoría de números y álgebra como la fórmula de Legendre, propiedades del sistema numérico combinatorio y la división polinómica.