Wiki Agenda Contact English version

Infinity of primes

A constructive proof that there is an infinity of primes

Auteurs: Jean-Christophe Filliâtre

Catégories: Mathematics

Outils: Why3

see also the index (by topic, by tool, by reference, by year)

A constructive proof that there is an infinity of primes

The idea is to build the sequence a(O) = 1 a(n) = a(n-1) * (a(n-1) + 1) and to show that a(n) has (at least) n distinct prime factors. See

Author: Jean-Christophe FilliĆ¢tre (CNRS)

use int.ComputerDivision
use number.Divisibility
use number.Prime

let lemma prime_factor (n: int) : (p: int)
  requires { n >= 2 }
  ensures  { prime p }
  ensures  { divides p n }
= for p = 2 to n do
    invariant { forall d. 2 <= d < p -> not (divides d n) }
    if mod n p = 0 then return p
  return n

use set.Fset

let lemma infinity_of_primes (n: int) : (s: fset int)
  requires { n >= 0 }
  ensures  { cardinal s = n }
  ensures  { forall k. mem k s -> prime k }
= let ref s = empty in
  let ref x = 1 in
  for i = 0 to n-1 do
    invariant { x >= 1 }
    invariant { cardinal s = i }
    invariant { forall k. mem k s -> prime k }
    invariant { forall k. mem k s -> divides k x }
    let p = prime_factor (x+1) in
    x <- x * (x+1);
    s <- add p s

download ZIP archive

Why3 Proof Results for Project "infinity_of_primes"

Theory "infinity_of_primes.Top": fully verified

ObligationsAlt-Ergo 2.4.0CVC4 1.7Z3 4.12.2
VC for prime_factor---------
loop invariant init---0.04---
loop invariant preservation---0.05---
out of loop bounds---0.03---
VC for infinity_of_primes---------
loop invariant init---0.04---
loop invariant init---0.06---
loop invariant init---0.05---
loop invariant init---0.06---
loop invariant preservation---0.07---
loop invariant preservation------8.31
loop invariant preservation---0.09---
loop invariant preservation0.05------
out of loop bounds---0.04---