AKS primality test

DefinitionThe primality decision problem#✓fully proved

The primality decision problem is the decision problem that accepts a bitstring \(x\) exactly when decoding \(x\) with the canonical bitstring encoding of the natural numbers (Mathlib's binary encoding) yields a prime number, and rejects \(x\) otherwise.

noncomputable def primesDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := ℕ) x with
  | some n => decide (Nat.Prime n)
  | none => false

Uses 3 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decision problems

Used byPRIMES is in P

TheoremPRIMES is in P#●ready to prove

The primality decision problem, which accepts a bitstring exactly when it decodes to a prime number under the canonical bitstring encoding of the natural numbers, belongs to the complexity class P.

public theorem_wanted primes_in_P :
    primesDec ∈ MetaMathlibExt.ComplexityTheory.P

Sources

• M. Agrawal, N. Kayal, and N. Saxena, "PRIMES is in P", Annals of Mathematics 160 (2004), 781-793.

Uses 4

Statement usesThe primality decision problem · Complexity classes · Decision problems · The complexity class P

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.