Agrawal's conjecture

Agrawal's conjecture is a stronger version of the theorem that forms the basis of the AKS primality test. If true, it would significantly improve the efficiency of primality testing.

The conjecture states that for coprime $n$ and $r$, if the polynomial congruence $(X-1)^n \equiv X^n-1 \pmod{n, X^r-1}$ holds, then $n$ is either prime or $n^2 \equiv 1 \pmod{r}$.

References:

• Wikipedia
• AIM Math
• Paper

theorem AgrawalConjecture.agrawal_conjecture : True ↔ ∀ (n r : ℕ), n > 1 → r > 0 → n.gcd r = 1 → let R := Polynomial (ZMod n); have X := Polynomial.X; have I := Ideal.span {X ^ r - 1}; (Ideal.Quotient.mk I) ((X - 1) ^ n) = (Ideal.Quotient.mk I) (X ^ n - 1) → Nat.Prime n ∨ ↑n ^ 2 = 1

Agrawal's Primality Conjecture.

Does the congruence $(X-1)^n \equiv X^n - 1 \pmod{n, X^r-1}$ imply $n$ is prime (with a specific exception for $n^2 \equiv 1 \pmod{r}$)?

While the "if" direction is a known theorem, the "only if" direction remains a conjecture.

theorem AgrawalConjecture.agrawal_conjecture.variants.popovych (n r : ℕ) : n > 1 → r > 0 → n.gcd r = 1 → let R := Polynomial (ZMod n); have X := Polynomial.X; have I := Ideal.span {X ^ r - 1}; (Ideal.Quotient.mk I) ((X - 1) ^ n) = (Ideal.Quotient.mk I) (X ^ n - 1) → (Ideal.Quotient.mk I) ((X + 2) ^ n) = (Ideal.Quotient.mk I) (X ^ n + 2) → Nat.Prime n ∨ ↑n ^ 2 = 1

Roman B. Popovych Conjecture. A stronger version of Agrawal's conjecture, which also considers the congruence $(X+2)^n \equiv X^n + 2 \pmod{n, X^r-1}$. If both congruences hold, then $n$ is either prime or $n^2 \equiv 1 \pmod{r}$. This variant was proposed by Roman B. Popovych in 2018.