John Harrison’s formalization of the AKS primality test

Freek Wiedijk University of Nijmegen

Intercity Number Theory Seminar Nijmegen

2003 06 06, 16:00

AKS

mathematics as we know it from proving primality after Agrawal-Kayal-Saxena by Daniel Bernstein:

Theorem 2.3 (2002.08.14; Manindra Agrawal, Neeraj Kayal, Nitin Saxena, and Hendrik W. Lenstra, Jr.). Let n, r, and v be positive integers. Let S be a finite set of integers. Assume that n and r are coprime; that n has order v modulo r; that gcd {n, b − b′} = 1 for all distinct b, b′ ∈ S; that ({#S+ϕ(r)−1 \atop #S}) ≥ n^{2d⌊\sqrt{ϕ(r)/d}⌋} for every positive integer d dividing ϕ(r)/v; and that (x + b)^{n} = x^{n} + b in the ring (Z/n)[x]/(x^{r} − 1) for all b ∈ S. Then n is a power of a prime.

key theorem of PRIMES ∈ P moving the theorem into the computer

!n r v s.
~(r = 1) /\
FINITE s /\
coprime(n,r) /\
(order(r) n = v) /\
(!b b'. b IN s /\ b' IN s /\ ~(b' = b)
        ==> (gcd(n,dist(b,b')) = 1)) /\
(!d. d divides (phi(r) DIV v)
     ==> binom(CARD s + phi(r) - 1,CARD s)
         >= n EXP (2 * d * ISQRT(phi(r) DIV d))) /\
(!b. b IN s
     ==> ((X + %b)^n === X^n + %b) (modulo {(%n),(X^r - %1)}))
==> ?p k. prime p /\ (n = p EXP k)

the context

John Harrison

got his PhD in Cambridge on automated theorem proving works at Intel proving Pentium chips correct formalizes mathematics for fun in his spare time

HOL Light HOL = Higher Order Logic

John Harrison’s re-implementation of the HOL proof assistant implemented in the ML programming language AKS formalization

• weak prime number theorem (done)

n ≥ 3 ⇒ \frac{1}{2} \frac{n}{ln n} ≤ π(n) ≤ 5\frac{n}{ln n}

• theory of cyclotomic polynomials (done)

• theorem 2.3 from Daniel Bernstein’s paper (work in progress)

• primality prover based on AKS (future)

• complexity analysis of the AKS algorithm (future) all proofs are fully formal all the way down to the axioms

HOL Light

the axioms

types

base types bool = {⊤, ⊥} ind = some infinite set function types A → B non-empty subtypes A′

type A + predicate in A → bool

objects

equality  =_{A}  ∈ A → A → bool
choice operator  @_{A}  ∈ (A → bool) → A

subtype mappings ∈ A′ → A ∈ A → A′

λ-terms λx. F [x] ∈ A → B logic examples of HOL objects

⊤ ∈ bool  ≡ (λx. x) =_{bool→bool} (λx. x)
∀_{A} ∈ (A → bool) → bool ≡ λP. (P =_{A→bool} (λx. ⊤))

no distinction between terms and statements, just λ-terms

∀x ∈ A. P [x] is represented by ∀_{A} (λx. P [x])

term = term
statement = term denoting an object in type bool
theorem = term denoting the object ⊤ in type bool

HOL logic is weaker than ZFC set theory (but not much)

‘functional programming’

a more mathematical way of programming Lisp, ML, Haskell

ML originally spin-off of the LCF proof assistant (predecessor of HOL)

example f^{n}(x)

#let rec funpow n f x =
  if n < 1 then x else funpow (n-1) f (f x);;
funpow : int -> ('a -> 'a) -> 'a -> 'a = <fun>
#funpow 6 (fun n -> 3*n-1) 1;;
- : int = 365
#

why should we trust a proof assistant?

very small ‘proof kernel’

de Bruijn criterion if you can trust the kernel, you can trust the whole system

HOL Light kernel

282 lines of ML only 9 pages (with many comments!)

HOL definitions

the shape of a formalization HOL files contain

• definitions (of HOL types, of HOL objects) minor part of the files: about 2%

• theorems (statements, each with a proof) major part of the files: about 80% long necklace of lemmas statements are readable formulas, proofs are unreadable ‘code’

• implementation of tactics small programs solve well-defined & mathematically trivial sub-problems examples of HOL types

num  = ℕ
int  = ℤ
real  = ℝ
complex  = ℂ

(A)list  = finite lists over the type A

(complex)list = ℂ [X]

int → int  = functions from ℤ to ℤ

intpoly  = ℤ[X]

intpoly → bool = the subsets of ℤ[X]

no parametrized type for polynomials over an arbitrary ring no type distinction between subsets of ℤ[X] and ideals of ℤ[X] ways to define a HOL function, variant I: abbreviations

let dist = new_definition
  `dist(m,n) = (m - n) + (n - m)`;;
let X = new_definition
  `X = mk_intpoly(\x. x)`;;

definitions using the Hilbert choice operator @ (‘epsilon’)

let ISQRT = new_definition
  `ISQRT n = @m. m EXP 2 <= n /\ n < (m + 1) EXP 2`;;
let aprimedivisor = new_definition
  `aprimedivisor q = @p. prime p /\ p divides q`;;

ways to define a HOL function, variant II: recursive definitions definition with recursion is built into HOL example

let EXP = new_recursive_definition num_RECURSION
 `(!m. m EXP 0 = 1) /\
  (!m n. m EXP (SUC n) = m * (m EXP n))`;;

recursion principle

num_RECURSION
|- !e f. ?fn. (fn 0 = e) /\ (!n. fn (SUC n) = f (fn n) n)

shows that the recursion is well-founded ways to define a HOL function, variant III: inductive definitions

inductive definitions (‘smallest set closed under … ’) also built into HOL

example

‘the ideal generated by a set s ⊆ ℤ[X]’

let idealgen_RULES,idealgen_INDUCT,idealgen_CASES =
  new_inductive_definition
  `(!x. s x ==> idealgen s x) /\
   idealgen s (%0) /\
   (!a b. idealgen s a /\ idealgen s b
          ==> idealgen s (a - b)) /\
   (!a x. idealgen s a ==> idealgen s (a * x))`;;
idealgen ∈ (intpoly → bool) → (intpoly → bool)

syntactic sugar

!n r v s.
~(r = 1) /\
FINITE s /\
coprime(n,r) /\
(order(r) n = v) /\
(!b b'. b IN s /\ b' IN s /\ ~(b' = b)
        ==> (gcd(n,dist(b,b')) = 1)) /\
(!d. d divides (phi(r) DIV v)
     ==> binom(CARD s + phi(r) - 1,CARD s)
         >= n EXP (2 * d * ISQRT(phi(r) DIV d))) /\
(!b. b IN s
     ==> ((X + %b)^n === X^n + %b) (modulo {(%n),(X^r - %1)}))
==> ?p k. prime p /\ (n = p EXP k)

‘(X + b)^{n} = X^{n} + b in the ring (ℤ/nℤ)[X]/(X^{r} − 1)’

   ((X + %b)^n === X^n + %b) (modulo {(%n),(X^r - %1)})

functions

         %  ∈ num → intpoly
 {(%n),(X^r - %1)} ∈ intpoly → bool

let intpolycong = new_definition
  `(p === q) (j:intpoly->bool) = (p - q) IN j`;;
let modulo = new_definition
  `modulo = idealgen`;;

note: this talks about polynomials in ℤ[X] instead of (ℤ/nℤ)[X] some AKS statistics

outside AKS  inside AKS
HOL type definitions  17  1 ← intpoly
HOL function definitions  308  45
theorems + proofs  2811  377
ML functions (tactics)  1222  14

currently the AKS files are about 1/7 th the size of the basic library

zooming in on a (trivial) lemma

the 10 HOL files of AKS

cyclotomic.ml  cyclotomic polynomials
isqrt.ml  integer square root
intpoly.ml  ring of univariate integer polynomials
fermatpoly.ml  Fermat’s Little Theorem for polynomials
psi.ml  analysis of Chebyshev’s ψ
7% → theta.ml  similar analysis of θ
bertrand.ml  Bertrand conjecture, just for fun
weakpnt.ml  Weak Prime Number Theorem, just for fun
findr.ml  use PNT to provide upper bound on r
aks.ml  the actual AKS theorem

7814 lines of code, 377 theorems π, θ, ψ

π(n) = ∑_{p≤n} 1  counts the primes ≤ n
θ(n) = ∑_{p≤n} ln p  sum over all primes ≤ n
ψ(n) = ∑_{p^{k}≤n} ln p  sum over all prime-powers ≤ n

examples π(6) = 1 + 1 + 1 = 3 θ(6) = ln(2) + ln(3) + ln(5) = ln(30) = 3.40120 ψ(6) = ln(2) + ln(3) + ln(2) + ln(5) = ln(60) = 4.09434

π(n) ∼ \frac{n}{ln n}  θ(n) ∼ n  ψ(n) ∼ n

theta.ml

1 definition

theta ∈ num → real

1 tactic

THETA_LIST : int -> thm list

[ ⊢ θ(n) = ln(…); ⊢ θ(n − 1) = ln(…); …; ⊢ θ(0) = ln(1) ]

called only once, for θ lower bound: THETA_LIST 412 12 theorems

main ones: PSI_THETA, THETA_LBOUND_1_2, THETA_UBOUND_3_2

θ(n) + ψ(⌊\sqrt{n}⌋) ≤ ψ(n) ≤ θ(n) + 2ψ(⌊\sqrt{n}⌋)

n ≥ 5 ⇒ \frac{1}{2}n ≤ θ(n) ≤ \frac{3}{2}n

THETA_LE_PSI, the smallest proof from theta.ml

let THETA_LE_PSI = prove
(`!n. theta(n) <= psi(n)`,
GEN_TAC THEN REWRITE_TAC[theta; psi] THEN
MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `p:num` THEN
STRIP_TAC THEN ASM_CASES_TAC `prime p` THEN
ASM_REWRITE_TAC[MANGOLDT_POS] THEN
ASM_SIMP_TAC[mangoldt; PRIME_PRIMEPOW] THEN
SUBGOAL_THEN `aprimedivisor p = p`
 (fun th -> REWRITE_TAC[th; REAL_LE_REFL]) THEN
ASM_MESON_TAC[APRIMEDIVISOR_PRIMEPOW; EXP_1; LE_REFL]);;

HOL proofs are unreadable all-capital ‘code’ (if you want formal proofs to be readable: use the Mizar proof assistant) proving with tactics: the system keeps a ‘proof obligation’

it : goalstack = 1 subgoal (1 total)
`!n. theta n <= psi n`
#e GEN_TAC;;
it : goalstack = 1 subgoal (1 total)
`theta n <= psi n`
#e (REWRITE_TAC[theta; psi]);;
it : goalstack = 1 subgoal (1 total)
`Sum (1,n) (\p. if prime p then ln (&p) else &0) <=
 Sum (1,n) (\d. mangoldt d)`
#e (MATCH_MP_TAC SUM_LE);;

… the 10 theorems that the proof refers to

theta   !n. theta n = Sum (1,n)

                      (\p. if prime p then ln (&p) else &0)

  psi   !n. psi n = Sum (1,n) (\d. mangoldt d)
SUM_LE   !f g m n. (!r. m <= r /\ r < n + m ==> f r <= g r)

                  ==> Sum (m,n) f <= Sum (m,n) g

MANGOLDT_POS   !d. &0 <= mangoldt d
mangoldt   !d. mangoldt d =

            (if primepow d then ln (&(aprimedivisor d))
                           else &0)

PRIME_PRIMEPOW   !p. prime p ==> primepow p
REAL_LE_REFL   !x. x <= x
APRIMEDIVISOR_PRIMEPOW   !p k. prime p /\ 1 <= k

              ==> (aprimedivisor (p EXP k) = p)

EXP_1   !n. n EXP 1 = n
LE_REFL   !n. n <= n

the QED dream of the formalization of mathematics

some metrics of proof formalization

• formalization in space formalization is about 4 times as big as informal TEX source ‘de Bruijn factor’

• formalization in time formalization takes about 1 man-week for a textbook page systems the main current proof assistants for the formalization of mathematics

HOL Light (UK)  the most elegant system
Mizar (Poland)  the most mathematical system
Isabelle (UK/Germany)  the most all-round system
Coq (France) & NuPRL (US) the most constructive systems
PVS (US)  the most popular system

(disclaimer: opinions on these systems may vary) so why would anyone want to go to all this trouble? uses of formalized mathematics

• checking ‘debugging’ proofs

• clarifying making all definitions very precise making scopes of assumptions in proofs explicit finding dependencies between lemmas

another reason people are doing this (I think)

• crafting a complex artifact mathematical proof in its purest form