PRIMES is in P: the polynomial Fermat congruence, the introspective groups, and the correctness of the Agrawal-Kayal-Saxena algorithm

1. Motivation

Agrawal, Kayal, and Saxena's "PRIMES is in P" (Annals of Mathematics 160 (2004) 781-793) settled a question open since the birth of complexity theory: primality has an unconditional, deterministic, polynomial-time test. The paper's algorithm is elementary - six steps: reject perfect powers; fix a small r; reject trivial factor witnesses; accept small inputs; test the congruence (X + a)^n = X^n + a modulo X^r - 1 for a = 1, ..., ell; accept. The mathematical heart is Lemma 2.1, a generalization of Fermat's Little Theorem to polynomial rings: for n at least 2 and a coprime to n, n is prime if and only if (X + a)^n = X^n + a in Z_n[X]. The correctness of the harder direction runs through the introspective machinery of Section 4: for a prime factor p of n with o_r(p) > 1, the numbers of I = {(n/p)^i p^j} are introspective for the polynomials of P = {the products of the generators X, X+1, ..., X+ell}; the residues of I generate a group G modulo r of size t > log^2 n; the images of P generate a group G-cal in the field F = F_p[X]/(h), h an irreducible factor of the r-th cyclotomic polynomial over F_p; Lenstra's lower bound and the Kalai-Sahai-Sudan upper bound on the size of G-cal collide unless n is a power of p, and step 1 excludes prime powers, so n is prime. Section 5 bounds the arithmetic work: O~(log^(21/2) n), unconditionally.

The mission formalizes the paper's mathematical content in Lean 4. The goal statement is Theorem 4.1: the algorithm of the algorithm layer returns PRIME if and only if n is prime. The milestones are the ingredients in attack order: the polynomial Fermat characterization (Lemma 2.1); the lcm lower bound (Lemma 3.1); the existence of a small r with large order (Lemma 4.3); the closure of introspection under multiplication (Lemmas 4.5 and 4.6); Lenstra's injectivity bound (Lemma 4.7); the Kalai-Sahai-Sudan collision bound (Lemma 4.8); and the polynomial work bound of Section 5 (Theorem 5.1, in generous integer form).

The source document is the uploaded paper (annals-v160-n2-p12.pdf in the mission materials).

2. The formalization fragment and conventions

The formalization is a two-layer development in the namespace AKS. The polynomial layer (AKS_poly) carries the congruences: congruence (1) as an equality in Z_n[X], congruence (2) as divisibility by X^r - 1 in Z_n[X], Definition 4.4's introspection relation over F_p[X], and the set P of products of the generators. The algorithm layer (AKS_alg) carries the arithmetic scaffolding and the algorithm itself: the integer logarithm, the multiplicative order, the lcm of the first numbers, the perfect-power predicate, the search for r, the loop bound, the six-step decision function, the set I and the residue group G, and the work measure of Section 5.

The following choices are disclosed explicitly.

1. Compile verification by CI substitution. The authoring environment has no local Lean toolchain, so the compile check demanded by the mission is performed by the continuous integration of the repository (Lean 4.33 with Mathlib): all Lean code below was compiled there before this proposal was submitted, and the code attached to the items is byte-identical to the compiled modules.

2. The theorem drafts carry sorry. The eight theorem statements are submitted as drafts for human review; each proof body is a single sorry marking the work the mission proposes to complete. The compilation therefore succeeds with exactly one "declaration uses 'sorry'" warning per theorem file.

3. Generous integer encodings of the logarithms. The paper's real-valued log n appears in the algorithm only through the threshold o_r(n) > log^2 n of step 2 and the loop bound ell = floor(sqrt(phi(r)) log n) of step 5. The mission encodes both with logUp n = floor(log2 n) + 1, which is strictly larger than log2 n: step 2 searches for the smallest r with ordR r n > logUp(n)^2, and ell is the floor of the product of the square root of phi(r) and logUp n, encoded exactly as the floor of the square root of phi(r) logUp(n)^2. Both encodings are generous in the directions that preserve correctness: primes pass congruence (2) for every a and r, so a larger threshold and a longer loop never reject a prime; and for the converse the larger threshold and loop only strengthen the group bounds that force composites out. The integer bookkeeping of the final chain - floor(sqrt t) logUp n + 1 at least sqrt t log2 n - is part of the proposed work of the goal, with the generosity supplying the slack.

4. The algorithm layer transcribes the six steps literally, with computable searches inside provable windows and classical decision where only the extension matters. ordR r a is the least k < r with a^k = 1 (mod r) - the window k < r is faithful because every multiplicative order divides phi(r) < r - and 0 when gcd(a, r) > 1. smallestR n searches the window bounded by the r_exists milestone's bound. aksDecide is stated with classical decision (open Classical, noncomputable): no execution of the test is ever needed, only its extensional behavior. aksWork is a computable schoolbook work measure charging logUp(n)^6 for step 1, r(logUp n + 1) for the searches of steps 2 and 3, and ell r n (logUp n + 1)(r + 1)^2 for the congruence loop of step 5.

5. The groups are encoded by witness windows, and the two bounds are stated in the paper's forms. G is the Finset of residues modulo r of the numbers of I, encoded by the witness window i, j < r - faithful under the coprimality of n/p and p to r, because both orders then divide phi(r) at most r, so every residue of an I-number is achieved inside the window. Lemma 4.7 is stated in the paper's form: two distinct polynomials of P, both of degree less than t, map to distinct elements of F = F_p[X]/(h) (the field is AdjoinRoot h; the hypotheses carry h dividing X^r - 1, the primitivity - h not dividing X^k - 1 for 0 < k < r - irreducibility by instance, the introspectivity of I for P, and t at most the size of G). Lemma 4.8 is stated in the collision form: unless n is a power of p, there are m2 < m1 at most n^(floor(sqrt t)), colliding modulo r inside the bounded set I-hat, such that every image of P in F satisfies y^m1 = y^m2. The cardinality bookkeeping between these forms and the size of G-cal - stars-and-bars for the lower bound with the unique factorization of the generator products, and the root bound of a polynomial over a field for the upper - is carried by Mathlib and is part of the goal's proposed work.

6. The field F = F_p[X]/(h) is taken with its factor h as an explicit parameter. The statements do not construct h; they carry h dividing X^r - 1, primitivity, and irreducibility as hypotheses (the latter two as Fact-class instances). The existence of h - an irreducible factor of the r-th cyclotomic polynomial over F_p of degree o_r(p), the standard fact of Lidl and Niederreiter cited as [LN] - is part of the mission's proposed work toward the goal.

7. The "is in P" claim is anchored by an explicit work measure, with the bit-cost correspondence in prose. Milestone 7 bounds aksWork by C logUp(n)^15, a generous integer form of Theorem 5.1's O~(log^(21/2) n) - the generous exponent absorbs the schoolbook charging model and the logUp slack. The correspondence between arithmetic-work measures and Turing-machine bit complexity - the standard O~(m) arithmetic on m-bit numbers of the paper's Section 5 - is carried in prose; a machine-level formalization is out of scope.

8. Pruned content. The paper's Section 5 refinements (Fouvry's Lemma 5.2 and the O~(log^(15/2) n) of Theorem 5.3, and the Lenstra-Pomerance variant), the conjectures (Artin's, the Sophie Germain density, Conjecture 6.1), and the historical survey of Section 1 are out of scope; the mission carries the unconditional Section 5 analysis only, in generous integer form, and the correctness theorem (Theorem 4.1) as the goal.

9. Due diligence. Before creating the proposal, the creation script searches the platform for prior definitions and theorems matching the paper's ingredients; the search results are recorded in the repository's results directory for the reviewer.

10. Definition names and module stems. The two definition bundles are published under names equal to their module stems (AKS_poly, AKS_alg), so that the platform imports Definitions.Def_AKS_* in the theorem preambles resolve, in dependency order poly, then alg (which imports poly).

3. Formalization targets

The mission has ten items: two reference definitions and eight theorem drafts, in the following order.

Reference definitions (the formalization fragment):

• AKS_poly: the polynomial layer. Congruence (1) as the equality (X + a)^n = X^n + a in Z_n[X]; congruence (2) as divisibility by X^r - 1 in Z_n[X]; Definition 4.4's introspection relation over F_p[X]; and the set P of products of the generators X, X+1, ..., X+ell.
• AKS_alg: the algorithm layer. The integer logarithm logUp; the multiplicative order ordR; the lcm of the first numbers; the perfect-power predicate; the six-step decision function aksDecide with its search smallestR and loop bound ell; the set I and the residue group G; and the work measure aksWork.

Theorem drafts (milestones in attack order, then the goal):

1. AKS.poly_fermat: Lemma 2.1 - for n at least 2 and a coprime to n, n is prime if and only if (X + a)^n = X^n + a in Z_n[X] (Section 2).
2. AKS.lcm_lower: Lemma 3.1 - the lcm of the first m numbers is at least 2^m for m at least 7 (Section 3).
3. AKS.r_exists: Lemma 4.3 - for n > 1 there is an r with 1 < r at most max 3 (logUp n)^5 and ordR r n > logUp(n)^2 (Section 4).
4. AKS.introspective_closure: Lemmas 4.5-4.6 - introspective numbers are closed under products, and introspectivity is closed under products of polynomials (Section 4).
5. AKS.group_inj: Lemma 4.7 (Hendrik Lenstra Jr.) - two distinct polynomials of P, both of degree less than t, map to distinct elements of F = F_p[X]/(h), under the primitivity and introspectivity hypotheses, with t at most the size of the residue group G (Section 4).
6. AKS.group_upper: Lemma 4.8 (Kalai-Sahai-Sudan) - unless n is a power of p, there are m2 < m1 at most n^(floor(sqrt t)), colliding modulo r inside the bounded set I-hat, such that every image of P in F satisfies y^m1 = y^m2 (Section 4).
7. AKS.poly_time: the work bound - there is a constant C with aksWork n at most C logUp(n)^15 for every n, the generous integer form of Theorem 5.1 (Section 5).
8. AKS.prime_iff (the goal): Theorem 4.1 - aksDecide n = PRIME if and only if n is prime (Section 4).

Milestones 1 to 7 correspond to the theorem drafts 1 to 7; the goal is draft 8.

4. Significance

The paper is one of the landmark results of computational number theory: a problem open since the 1960s - an unconditional, deterministic, polynomial-time primality test - solved by elementary means, in a proof whose only ingredients are the binomial theorem, Euler's function, and the root bound of a polynomial over a field. The formal account forces exactly what the prose leaves to convention: the precise ring in which each congruence lives, the precise windows in which the searches find their witnesses, the precise generosity of each integer rounding, and the precise content of the two group bounds. The paper's difficulty lies not in any single deep theorem but in the assembly of many small lemmas under one bound chain; a formalization makes each link explicit and checkable, and the mission's readback discipline gives an independent restatement check of every statement before review.

5. Difficulty

Milestone 1 is a commutation: the forward direction is the freshman's dream in Z_p[X] plus Fermat's little theorem for the base; the backward direction isolates the coefficient of X^q for a prime q with q^k dividing n exactly and computes its q-adic valuation below k. Milestone 2 is Nair's argument: the product of the primes in (m/2, m] divides the lcm. Milestone 3 is the counting argument: every bad r divides a single product below the lcm of the window, so some r in the window escapes. Milestone 4 is two ring commutations: f^(m m') = f(X^(m m')) along f(X^m)^(m') = f(X^(m m')), and the product rule for introspectivity. Milestone 5 is Lenstra's argument: from a collision in F and introspection, f(Y) - g(Y) acquires the t distinct primitive r-th roots indexed by G, exceeding its degree. Milestone 6 is the pigeonhole of I-hat against G, the non-power distinctness, and the collision equation transported by introspection. Milestone 7 is arithmetic over the windows. The goal assembles: Lemma 4.2's direction is the congruences for primes; the step-4 case is the factor below the square root; and the step-6 case is the chain of Lemma 4.9 - the injectivity lower bound, the collision upper bound, and the integer bookkeeping that the generous encodings close with slack.

6. Scope

Included: the two congruences and the introspection relation; the set P and the set I with the residue group G; the six-step algorithm; and the eight statements - the Fermat characterization, the lcm bound, the small-r existence, the two closure lemmas, the two group bounds, the work bound, and the correctness theorem.

Excluded, as disclosed in items 7 and 8 of section 2: the machine-level bit-cost formalization of "is in P" (carried in prose, anchored by the explicit aksWork measure); the Section 5 refinements (Fouvry's Lemma 5.2, the O~(log^(15/2) n) of Theorem 5.3, the Lenstra-Pomerance variant of [LP1]); the conjectures of Section 5 and Conjecture 6.1; and the historical survey of Section 1.

7. References

• Manindra Agrawal, Neeraj Kayal, and Nitin Saxena, "PRIMES is in P", Annals of Mathematics 160 (2004) 781-793. The source document is the uploaded paper (annals-v160-n2-p12.pdf).
• M. Nair, "On Chebyshev-type inequalities for primes", American Mathematical Monthly 89 (1982) 126-129 (the reference for Lemma 3.1).
• Rudolf Lidl and Harald Niederreiter, Introduction to Finite Fields and their Applications, Cambridge University Press, 1986 (the reference [LN] for the factorization of the cyclotomic polynomial over F_p).
• Hendrik W. Lenstra Jr., "Primality testing with cyclotomic rings", unpublished, August 2002 (the source of Lemma 4.7).
• Adam Kalai, Amit Sahai, and Madhu Sudan, private communication, August 2002 (the source of the proof of Lemma 4.8).