Metamath Blueprint : AKS (PRIMES is in P)


PRIMES IS IN P

The AKS primality test (also known as Agrawal–Kayal–Saxena primality test and cyclotomic AKS test) is a deterministic primality-proving algorithm created and published by Manindra Agrawal, Neeraj Kayal, and Nitin Saxena, computer scientists at the Indian Institute of Technology Kanpur, on August 6, 2002, in an article titled PRIMES is in P.

The AKS primality test is based upon the following theorem:

Given an integer n \geq 2 and integer a coprime to n, n is prime if and only if the polynomial congruence relation

(X+a)^{n}\equiv X^{n}+a{\pmod {n}}

holds within the polynomial ring (\mathbb{Z}/n\mathbb{Z})[X].


intro1 aks61c6 rhmextex akslb aks10kbnd aks61c5 aks61c4 lcmineqlem odrlblem aks61c2 cl3 aks22 aks61c7 aks61c1 intro2 aks61 aks61c3 claim2p1 defintrospective aksthr aksth taylconcavebnd phibnd 3lexlogpow5ineq3 znzrhfo cl3contnpows fta1g prmfac1 dvdsfac