10.6092/issn.1972-5787/3406
We discuss the formalization, in the Matita Interactive Theorem Prover, of some results by Chebyshev concerning the distribution of prime numbers, subsuming, as a corollary, Bertrand's postulate. 
Even if Chebyshev's result has been later superseded by the stronger prime number theorem, his machinery, and in particular the two functions psi and theta still play a central role in the modern development of number theory. The proof makes use of most part of the machinery of elementary arithmetics, and in particular of properties of prime numbers, gcd, products and summations, providing a natural benchmark for assessing the actual development of the arithmetical knowledge base.
application/pdf
1972-5787
3406
1
en
Wilmer Ricciotti
Journal of Formalized Reasoning
A proof of Bertrand's postulate
Text.Serial.Journal
https://jfr.unibo.it/
5
Articles
2012-12-30
2013-01-07
2012-12-30
2016-01-29
37-57
JFR
Wilmer Ricciotti
2012/12/30
10.6092/issn.1972-5787/3406
37
University of Bologna
1972-5787
1
en
57
A proof of Bertrand's postulate
https://jfr.unibo.it/article/download/3406/2771
5
A proof of Bertrand’s postulate
Andrea Asperti, Wilmer Ricciotti
Dipartimento di Scienze dell’Informazione
Università degli Studi di Bologna


We discuss the formalization, in the Matita Interactive Theorem Prover, of some results by Cheby-
shev concerning the distribution of prime numbers, subsuming, as a corollary, Bertrand’s postulate.
Even if Chebyshev’s result has been later superseded by the stronger prime number theorem, his
machinery, and in particular the two functions ψ and θ still play a central role in the modern
development of number theory. The proof makes use of most part of the machinery of elementary
arithmetics, and in particular of properties of prime numbers, gcd, products and summations, pro-
viding a natural benchmark for assessing the actual development of the arithmetical knowledge
base.




1.   INTRODUCTION
Bertrand’s postulate states that for every natural number n larger than 1 there is
always at least one prime p such that n < p ≤ 2n.
   The statement was first conjectured by Joseph Bertrand 1945, who also verified
his correctness for all numbers up to 3 · 106 . A first complete proof was given
by Chebyshev in 1850; alternative proofs have been given by Ramanujan in 1919
[17], using properties of the Gamma function, and by Erdös in 1932 [10], exploiting
Chebyshev’s function θ. So, even if Bertrand’s postulate is subsumed by the prime
number theorem of Hadamard and la Vallé Poussin (1896), it has an interest in its
own, and in particular it makes very precise claims about the distribution of primes
for small values of n.
   The prime number theorem (PNT) affirms that the number of primes π(n) not
exceeding n is asymptotically equal to n/ log(n) (see e.g. [16, 20] for a modern
introduction to the subject). As a consequence, the number of primes between n
and 2n grows as n/log(n) when n is large, and hence there are many more primes
in this interval than asserted by Bertrand’s Postulate.
   Chebyshev original proof follows a similar approach, but relying on a weaker prop-
erty than PNT, namely that the order of magnitude of π(n) is n/ log n (Chebyshev’s
theorem), meaning that we can find two positive constants c1 and c2 such that, for
any n
                                   n                  n
                              c1        ≤ π(n) ≤ c2
                                 log(n)             log n
Then, if a > c2 /c1 .
                                        an           n     (ac1 − c2)n
                π(an) − π(n) ≥ c1             − c2       ≥             >0
                                      log(2n)      log n     log(2n)
so we are sure to have at least a prime between n and an. If (for sufficiently large
n) we are able to prove that c2 < 2c1 , then Bertrand’s conjecture follows.

                                        Journal of Formalized Reasoning Vol. 5, No. 1, 2012, Pages 37–57.
38     ·     A. Asperti and W. Ricciotti

   Even if Chebyshev’s theorem is sensibly simpler than the prime number theorem,
already formalized by Avigad et al. in Isabelle [8] and by Harrison in HOL Light
[15], it is far from trivial (in Hardy and Wright’s famous textbook [13], it takes
pages 340-344 of chapter 22). The proof makes use a lot of machinery of elementary
arithmetics, and in particular of properties of prime numbers, gcd, products and
summations, providing a natural benchmark for assessing the actual development
of the arithmetical knowledge base in proof assistants, and for comparing them.
   We were also interested in providing a fully arithmetical (and constructive) proof
of this theorem. Even if Selberg’s proof of the prime number theorem is “elemen-
tary”, meaning that it requires no sophisticated tools of analysis except for the
properties of logarithms, a fully arithmetical proof of this results looks problem-
atics, considering that the statement involves in an essential way the Naperian
logarithm. On the other side, the logarithm in Chebyshev’s theorem can be in any
base, and can be also essentially avoided (at least from the statement), asserting
the existence of two constants c1 and c2 such that, for any n
                                      2c1 n ≤ nπ(n) ≤ 2c2 n
that is what we actually proved.
   For the proof of Bertrand’s postulate we followed instead Erdös argument, that is
particularly elegant and allows us to take advantage of the computational facilities
of the proof assistant Matita.
   This paper is an extended and largely revised version of our previous work [3].
In particular, the proof assistant Matita [5], that we used for the formalization,
has meanwhile undergone a substantial evolution, giving us the opportunity to
make a detailed comparison between the two versions, and to discuss the many
improvements introduced in the new system.
   The structure of the paper is the following. In Section 2 we discuss some impor-
tant preliminaries behind the formal proof, and in particular the new library of big
operators of Matita. Section 3 is devoted to some considerations about the factor-
ization of n!; in particular, we exploit the decomposition   of (2n)! as n!2 · B(2n),
                                           2n
                                              
where B(2n) is the binomial coefficient n , and study upper and lower bounds
for B(2n). Section 4 contains the definition of Chebyshev’s Ψ function and the
proof of the asymptotic distribution of the prime numbers. Finally, Section 5 is de-
voted to the proof of Bertrand’s postulate, comprising a discussion of Chebyshev’s
θ function.

2.   PRELIMINARIES
In the rest of the paper, all functions are defined on natural numbers. In particular,
n/m denotes the integer part of the division between n and m, and loga n denotes
the maximum i such ai ≤ n. We shall use the notation n! for the factorial of n,
that is the product of all positive numbers below or equal to n.
                                             Y
                                       n! =      i                                 (1)
                                                   i≤n

Chebyshev’s approach to the study of the distribution of prime numbers consists
in exploiting the decomposition of n! as a product of prime numbers. The idea is
that the numbers 1, 2, . . . , n include just np multiples of p, pn2 multiples of p2 , an so
Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
2     PRELIMINARIES                                                                   39

on. Hence
                                      Y     Y               i+1
                               n! =                  pn/p                             (2)
                                      p≤n i<logp n

A formal proof of the previous sentence consists in a symbolic manipulation of
expressions on “big products”, allowing us to pass from equation 1 to equation 2.
This kind of manipulations are an easy task for a mathematician, but are relatively
complex operations to be performed inside a proof assistant, requiring a large library
of lemmas covering not trivial operations such as reindexing and commutation.
   It is only in relatively recent times that the importance of a good library of
canonical big operators has been duly emphasized as one of the key ingredients
behind a really usable library of formal mathematics [9]. In this section, we shall
briefly describe the new “bigops” library of Matita, comprising both notations
covering in a uniform way different form of indexing, and lemmas encapsulating
the most frequent logical steps on these constructs.
   The library relies on Matita’s mechanism of unification hints [4, 19] for expressing
structural and algebraic properties of indices and operators. This allows rewriting
and resolution to infer such properties automatically, which is essential for the
practical usability of the library.
   In particular, unifications hints are used, similarly to canonical structures in
[9], to enrich concrete operations to meet the algebraic requirements (associativity,
commutativity, etc. ) of generic operators in parametric lemmas.
   For instance, consider decomposition laws like the following, where a ≤ b ≤ c
            X          X          X             Y          Y          Y
                 fi =       fi +      fi             fi =       fi ·       fi
          i∈[a,c]    i∈[a,b]    i∈[b,c]          i∈[a,c]          i∈[a,b]   i∈[b,c]

One would like to express them in a generic way, for an arbitrary operator op to
be instantiated with + and ·, respectively. However, the abstract law is true only
if the operator is associative. As discussed in [9], the best approach is to define the
notion of “associative operation”, that is just a record composed by a function and
a proof that the function is associative, and to state the abstract property for a
generic “associative operation”.
   Then, we use the mechanism of unification hints to suggest to Matita that, if
it meets a sum, and if required by unification, it may lift it up to an associative
operation using some laws suggested by the user.
   Note that, a priori, this is a narrowing operation [11], and it would be a quite
complex operation to be performed automatically by the system without some hint
from the user).
   The basic machinery of big operators was already in the old version of Matita
(see e.g. [2]); however, we were lacking the mechanism of proof hints, essentially
forcing us to replicate the statement of most lemmas for each specific operator.
2.1    Notation
The notation for a generic big operator must be parametric in the range, in the
function F applied on elements in the range, in the operator op used to combine
them, and in the value nil to be returned when the range is empty.
  The notation is relatively standard ([9]), and has the following shape:
40     ·     A. Asperti and W. Ricciotti

                                                                                      
\big [ op / nil ] { range description } F
                                                                                      
   The range description is responsible for giving the name of the bound variable
and stating the set over which this variable is supposed to range. The elements
in the range are supposed to be enumerated (that is not a limitation, considering
that the range must be finite), hence the range is specified as an interval i ∈ [a, b[
where a is the lower bound (included in the range) and b is the upper bound (not
included in the range). In case the lower bound is 0, the simpler notation i < b can
also be used. The variable i whose name can obviously be chosen by the user, is
bound by the notation, and its scope ranges over F .
   Following our old library of generic iterators (see [2]), we add the possibility to
filter the range with a boolean predicate, meaning that the big operator takes only
the elements of the range that satisfy the predicate. This is simply written by
adding | P at the end of the index and range description. Again, the scope of
the bound variable i ranges over the formula P. For instance, the following notation
represents the product of all primes less or equal to n (that is essentially Chebyshev
θ function).
                                                                                      
\big[times/1] {p < S n | primeb p} p
                                                                            
The primitive operator is \big[op/nil]_{i < n | p i} f i, implemented by the
following code, whose reading is straightforward
                                                                            
 let rec bigop (n:nat) (p:nat → bool) (B:Type[0])
    ( nil : B) (op: B → B → B) (f: nat → B) :=
   match n with
    [ O ⇒ nil
    | S k ⇒ match p k with
        [true ⇒ op (f k) (bigop k p B nil op f)
        | false ⇒ bigop k p B nil op f]
    ].
                                                                                       
We also provide special notation in case the operator satisfies a particular structure.
In particular, in case the operator is the sum or the product on P   natural numbers,
                                                                                    Q
the user can use the more readable and comfortable notations            (\sum) and
(\prod) as abbreviations for, respectively, \big[plus\0] and \big[times\1].
2.2   Main Lemmas
The library of results concerning big operators is naturally organized according to
the assumptions on the operator being iterated.
   A first collection of lemmas, mostly relative to subsuming equalities on big op-
erators from equalities of its components, do not require any assumption on the
operator. The following is a typical example, expressing the fact that we can
rewrite in the predicate and the formula parts of a big operation without changing
its semantics:
                                                                                   
lemma same bigop : ∀k,p1,p2,B,nil,op.∀f,g:nat→ B.
  sameF upto k bool p1 p2 → sameF p k p1 B f g →
  \big[op, nil ] {i < k | p1 i}(f i ) = \big[op,nil ] {i < k | p2 i}(g i ).
                                                                                      
Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
2    PRELIMINARIES                                                                        41

  The first premise sameF_upto k bool p1 p2 expresses the fact that the two
predicates p1 and p1 must coincide (pointwise) in the interval [0, k[; the second
condition sameF_p k p1 B f g requires that the two functions f and g coincide
pointwise in the range {i < k | p1 i} (that is the same as {i < k | p2 i}).
  A second collection of lemmas allow to change the length of the range. A typical
case is to restrict the bound when it is known that the filtering predicate is false
on the eliminated part.
                                                                                    
theorem pad bigop1: ∀k,n,p,B,nil,op.∀f:nat→ B. n ≤ k →
  (∀i . n ≤ i → i < k → p i = false) →
  \big[op, nil ] {i < n | p i}(f i ) = \big[op,nil ] {i < k | p i}(f i ).
                                                                                              
   More interesting decompositions can be obtained in case the operator is associa-
tive. For example, we can use the following lemma to decompose an interval in two
parts:
                                                                                   
theorem bigop sumI: ∀a,b,c,p,B.∀nil.∀op:Aop B nil.∀f:nat→ B.
a ≤b →b ≤c →
\big[op, nil ] {i ∈ [a,c[ | p i}(f i ) =
  op (\big[op, nil ] {i ∈ [b,c[ | p i}(f i )) (\big[op, nil ] {i ∈ [a,b[ | p i}(f i )).
                                                                                              
    Aop is the type of associative operators, defined in the following way:
                                                                                              
record Aop (A:Type[0]) (nil:A) : Type[0] :=
  {op :2> A → A → A;
   nill :∀a. op nil a = a;
   nilr :∀a. op a nil = a;
   assoc: ∀a,b,c.op a (op b c) = op (op a b) c
  }.
                                                                                        
   A slightly more complex theorem, that plays a crucial role for the commutation
of bigops, is the following one, exploiting the decomposition of an integer i in the
range [0, k1 × k2 [ as a pair hi/k2 , i mod k2 i where the first component ranges in the
interval [0, k1 [ and the second one in the interval [0, k2 [.
                                                                                        
theorem bigop prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat → nat → B.
\big[op, nil ] {x<k1|p1 x}(\big[op,nil] {i<k2|p2 x i}(f x i )) =
  \big[op, nil ] {i<k1∗k2|andb (p1 (i/k2)) (p2 (i/k2) (i \mod k2))}
     ( f ( i/k2) ( i \mod k2)).
                                                                                    
  Things become really interesting when the operator is also commutative, since in
this case the order in which elements in the range are processed becomes irrelevant.
  For instance, a very useful lemma is the following one, allowing to single out a
specific element i from the range, processing it independently:
                                                                                    
lemma bigop diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
  i < n → p i = true →
  \big[op, nil ] {x<n|p x}(f x)=
    op (f i ) (\big[op, nil ] {x<n|andb(notb(eqb i x))(p x)}(f x)).
                                                                                              
  Another, more general one states that the semantics of the bigops is the same,
provided the ranges are isomorphic.
42      ·    A. Asperti and W. Ricciotti

                                                                                     
theorem bigop iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
  iso B (mk range B f1 n1 p1) (mk range B f2 n2 p2) →
  \big[op, nil ] {i<n1|p1 i}(f1 i ) = \big[op,nil ] {i<n2|p2 i}(f2 i ).
                                                                                  
  As a corollary, we obtain the following commutation result, extremely useful for
our development.
                                                                                  
theorem bigop commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:ACop B nil.∀f.
0 < n →0 < m →
(∀i , j . i < n → j < m → (p11 i ∧ p12 i j) = (p21 j ∧ p22 i j )) →
\big[op, nil ] {i<n|p11 i}(\big[op, nil ] {j<m|p12 i j}(f i j )) =
   \big[op, nil ] {j<m|p21 j}(\big[op,nil] {i<n|p22 i j}(f i j )).
                                                                                     
  A final set of lemma is devoted to distributivity. In this case, we expect to have
two operators sum and prod, such that sum is associative and commutative, and
prod distributes over sum:
                                                                                    
record Dop (A:Type[0]) (nil:A): Type[0] :=
  {sum : ACop A nil;
   prod: A → A → A;
   null : \ forall a. prod a nil = nil ;
   distr : ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
  }.
                                                                                     
     One of the main results is the following one, whose reading is immediate:
                                                                                     
theorem bigop distr: ∀n,p,B,nil.∀R:Dop B nil.∀f,a.
  let aop :=sum B nil R in
  let mop :=prod B nil R in
  mop a \big[aop,nil] {i<n|p i}(f i ) =
   \big[aop, nil ] {i<n|p i}(mop a (f i )).
                                                                                     

3.    PRIMES AND THE FACTORIAL FUNCTION
As we already said, the starting point of Chebyshev was the following decomposition
of the factorial of n (see e.g. [13], p. 342).
                                       Y Y          i+1
                                 n! =          pn/p                             (3)
                                          p≤n i<logp n

Giving a formal proof of the previous statement requires some work, starting from
the definition of the order of a prime p in a number n, and the properties of this
function.
3.1    Order of a prime
Every integer n may be uniquely decomposed as the product of all its prime factors.
For our purposes, we also need to take into account the so called order ord p n of
each prime p in n, that is the multiplicity of p as a factor of n.
  This function can be algorithmically defined by iterating the division operator
until (n mod p) 6= 0, increasing a counter at each iteration. However, since Matita
only accepts well founded recursive definitions, we also need to provide an upper
Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
3     PRIMES AND THE FACTORIAL FUNCTION                                             43

bound k to the number of iterations (that in is this case can initialized to n itself).
It is also convenient to compute, at the same time with the order of p in n, the
remainder of n after removing all p-factors.
                                                                                       
 let rec p ord aux k n p :=
   match n \mod p with
   [ O ⇒
     match k with
       [ O ⇒ hO,ni (∗ dummy ∗)
       | S k0 ⇒ let hq,ri :=p ord aux k0 (n / p) m in hS q,ri]
   | S ⇒ hO,ni].

(∗ p ord n p = <q,r> if p divides n q times, with remainder r ∗)
definition p ord :=λn,p:nat.p ord aux n n p.

definition ord :nat → nat → nat :=λn,p. fst ?? (p ord n p).

definition ord rem :nat → nat → nat :=λn,p. snd ?? (p ord n p).
                                                                                 
  The behavior of the previous functions is essentially captured by the following
theorems, but a small library of about 30 lemmas help to work with them in a
comfortable way.
                                                                                 
theorem exp ord: ∀p,n. 1 < p → O < n →
  n = pˆ(ord n p) ∗ (ord rem n p).
                                                                                        
                                                                                        
theorem not divides ord rem: ∀m,p.O < m → 1 < p →
  p 6 | (ord rem m p).
                                                                                        
                                                                                   i+1
  The following result characterizes the order of p in n as the number of times p
divides n.
                                                                                        
theorem eq ord sigma p: ∀n,m,p. O < n → prime p →
  pˆm ≤ n → nP< pˆ(S m) →
    ord n p =   {i < m | dividesb (pˆ(S i)) n} 1.
                                                                                        

3.2    Factorization
With the help of the order function, the factorization of a natural number n can
now be expressed in the following way:
                                                                                
     Q factorization: ∀n. O < n →
theorem
  n=    { p < (S n) | primeb p}(pˆ(ord n p)).
                                                                                   
The idea for proving the previous result is to work by induction on the upper
bound of the product, namely n; the problem is that n appears many times in
the statement with different roles, and a brute force approach would not provide
the suitable induction hypothesis. We need first to generalize a bit the statement,
making the bound more independent from the integer being factorized. In fact, the
statement remains true provided the range of the product covers any prime that is
a divisor of n, and we can take as an upper bound their maximum:
44     ·     A. Asperti and W. Ricciotti

                                                                                     
lemma max to factorization: ∀q,m. O<m →
         m) (λi.primeb i ∧ dividesb i m)<q →
  max (S Q
   m=      {p < q | primeb p ∧ dividesb p m} (pˆ(ord m p)).
                                                                                    
This result can now be proved by induction on m: the proof is not entirely straight-
forward (it takes about 100 lines in Matita) but it does not present any major
conceptual difficulty.
3.3   Factorial
The factorial function is defined in matita in a recursive way:
                                                                                     
let rec fact n :=
  match n with [ O ⇒ 1 | S m ⇒ fact m ∗ S m].
                                                                                   
For our purposes we need however to exploit its representation in the form of a big
product (a theorem that is easily proved by induction on n):
                                                                                   
theorem eqQfact pi:∀n.
  fact n =   {i ∈[1,S n[ } i .
qed.
                                                                              
We have now the right machinery to prove Chebyshev’s decomposition of the fac-
torial function of equation 2. Formally:
                                                                              
theorem Qfact pi decomp: ∀n.      Q
fact n =    { p < S n | primeb p}( {i < log p n} (pˆ(n /(pˆ(S i))))).
                                                                                     
The proof ( 130 lines) is summarized by the following chain of equations:
                                  Y
                            n! =       m
                                         1≤m≤n
                                           Y     Y         Y
                                     =                                    p
                                         1≤m≤n p≤m i < logp m
                                                     pi+1 |m
                                         Y     Y          Y
                                     =                                    p
                                         p≤n p≤m≤n i < logp m
                                                     pi+1 |m
                                         Y     Y         Y
                                     =                               p
                                         p≤n i<logp n m ≤ n
                                                      pi+1 |m
                                         Y     Y               i+1
                                     =                  pn/p
                                         p≤n i<logp n

In particular, for 2n we have:
                                           Y       Y                     i+1
                                (2n)! =                    p2n/p                (4)
                                          p≤2n i<logp 2n




Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
3     PRIMES AND THE FACTORIAL FUNCTION                                              45

                                2n
Let us decompose               pi+1   in the following way:
                                                                               
                                         2n         n       2n
                                         i+1
                                             =  2  i+1
                                                       +                mod 2
                                        p         p        pi+1
Moreover, if n ≤ p or logp n ≤ i we have
                                                     n
                                                         =0
                                                    pi+1
Hence, if we define
                                               Y     Y                i+1
                                      B(n) =                  p(n/p         mod 2)

                                               p≤n i<logp n

equation (4) becomes
                                 (2n)! = n!2 B(2n)                                   (5)
B(2n) is thus the binomial coefficient 2n
                                          
                                        n .
The formal definition of B in Matita looks as follows:
                                                                                          
definition
 Q         B :=λn.        Q
     {p < S n | primeb p}( {i < log p n} (pˆ((n /(pˆ(S i))) \mod 2))).
                                                                               
It is worth to remark that the definition is computable; these are some typical
values of B, for small integers:
                                                                               
example   B   3:   B   3   =   6. // qed.
example   B   4:   B   4   =   6. // qed.
example   B   5:   B   5   =   30. // qed.
example   B   6:   B   6   =   20. // qed.
example   B   7:   B   7   =   140. // qed.
example   B   8:   B   8   =   70. // qed.
                                                                                          
Equation 4 is expressed by the following theorem:
                                                                                          
theorem eq fact B:∀n. 1 < n → (2∗n)! = n!ˆ2 ∗ B(2∗n).
                                                                                          

3.4    Upper and lower bounds for B
The next step is to provide upper and lower bounds for B.
  It is well known that, for any n, (2n)! ≤ 22n−1 n!2 . For technical reasons, we need
however a slightly stronger result, namely,
                                                (2n)! ≤ 22n−2 n!2
that holds for any n larger than 4.
                                                                                          
theorem lt 4 to fact: ∀n.4<n → (2∗n)! ≤ 2ˆ((2∗n)−2)∗n!∗n!.
                                                                               
The proof is by induction on n.
The base case amounts to check that 10! ≤ 28 5!2 , that can be proved by a mere
computation (after a few simplifications).
46     ·     A. Asperti and W. Ricciotti

In the inductive case
                         (2 · (n + 1))! = (2n + 2)(2n + 1)(2n)!
                                         ≤ (2n + 2)(2n + 1)22n−2 n!2
                                         ≤ (2n + 2)(2n + 2)22n−2 n!2
                                         = 22n (n + 1)!2
So, by equation (5), we conclude that, for any n
                                         B(2n) ≤ 22n−1                          (6)
and when n is larger than 4,
                                         B(2n) ≤ 22n−2                          (7)
                                                                                     
theorem lt 4 to le B exp: ∀n.4 < n → B (2∗n) ≤ 2ˆ((2∗n)−2).
                                                                                     
Similarly, we establish the following lower bound for the factorial function:
                                                                                     
theorem exp to fact2: ∀n.O < n → 2ˆ(2∗n)∗n!ˆ2 ≤ 2∗n∗(2∗n)!.
                                                                                     
The proof is by induction on n. For n = 1 both sides reduce to 4. For n > 1,
                     22n+2 (n + 1)!2 = 4(n + 1)2 22n n!
                                        = 4(n + 1)2 2n(2n)!
                                        = 4(n + 1)(n + 1)2n(2n)!
                                        ≤ 4(n + 1)(n + 1)(2n + 1)(2n)!
                                        = 2(n + 1)(2n + 2)(2n + 1)(2n)!
                                        = 2(n + 1)(2n + 2)!
By equation (5), we finally obtain our lower bound for B:
                                                                                     
theorem le exp B: ∀n. O < n. 2ˆ(2∗n) ≤ 2 ∗ n ∗ B (2∗n).
                                                                                     
Since for any n, 2n ≤ 2n , we also have
                                           2n ≤ B(2n)                           (8)
but this is less precise and less useful.

4.   CHEBYSHEV’S Ψ FUNCTION
Let prim n be the function that counts the number of prime numbers below n
(included). A possible definition of prim is the following:
                     P
                                                                           
definition prim :=λn.         {i < S n | primeb i} 1.
                                                                                     
Let us now consider the following function
                                        Y
                                Ψ(n) =     plogp n
                                                 p≤n

where the product ranges over all primes less or equal to n.

Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
4   CHEBYSHEV’S Ψ FUNCTION                                                                  47

                                                                                                 
definition
     Q     Psi: nat → nat :=
 λn. {p < S n | primeb p} (pˆ(log p n)).
                                                                                    
Actually, Chebyshev’s ψ function is the naperian logarithm of our function Ψ, but
as we mentioned in the introduction, we prefer to avoid the use of logarithms as far
as possible.
As usual, the function Ψ is computable:
                                                                                    
example   Psi   1:   Psi   1   =   1. // qed.
example   Psi   2:   Psi   2   =   2. // qed.
example   Psi   3:   Psi   3   =   6. // qed.
example   Psi   4:   Psi   4   =   12. // qed.
                                                                                                 
The relation between Ψ and π should be clear; since
                                                    plogp n ≤ n
we immediately get
                                                                                                 
theorem le Psil: ∀n. Psi n ≤ nˆ(prim n).
                                                                                                 
                                   loga n+1                       2 loga n
Moreover, since n < a                         , we also have n < a           , and hence
                                                                                                 
theorem lePsi r2: ∀n. nˆ(prim n) ≤ Psi n ∗ Psi n.
                                                                                                 
Let us now rewrite Psi n in the following equivalent form:
                                                                                                 
      Q Psi ’: nat → nat := Q
definition
 λn.     {p < S n | primeb p} ( {i < log p n} p).
                                                                                                 
We can easily prove
                                                                                                 
theorem eq Psi Psi’: ∀n.Psi n = Psi’ n.
                                                                                                 
and it is then clear, by the definition of B and P si0 , that
                                                                                                 
theorem le B Psi: ∀n. B n ≤ Psi n.
                                                                                                 
Hence, the lower bound for B immediately gives a lower bound for Ψ, namely


                                               2n ≤ 22n /2n ≤ Ψ(2n)                         (9)
For the upper bound, let us first observe that
                                       Y      Y
                       Ψ(2n) = Ψ(n)                                    pj(n,p,i)           (10)
                                                      p≤2n i<logp 2n
48     ·     A. Asperti and W. Ricciotti

where j(n, p, i) is 1 if n < pi+1 and 0 otherwise. Indeed
                        Y     Y
         Ψ(2n) =                    p
                          p≤2n i<logp 2n
                                                                                    
                              Y       Y                      Y      Y
                     =                      pj(n,p,i)                     p1−j(n,p,i) 
                            p≤2n i<logp 2n                  p≤2n i<logp 2n
                                  Y       Y
                     = Ψ(n)                     pj(n,p,i)
                               p≤2n i<logp 2n

Formally, this is stated by the following result (the formal proof takes about 50
lines).
                                                                                 
theorem eq Psi 2 n: ∀n.O < n →
Psi(2∗n)
  Q      =                   Q
     {p <S (2∗n) | primeb p}( {i <log p (2∗n)} (pˆ(leb (S n) (pˆ(S i))))) ∗ Psi n.
                                                                                 
where the boolean expression (leb (S n) (p^(S i))) is automatically converted
to an integer through an implicit coercion mapping false to 0 and true to 1.
Then, observe that
           Y      Y                         Y    Y          i+1
                       pj(n,p,i) ≤ B(2n) =            p(2n/p    mod 2)
                                                                             (11)
            p≤2n i<logp 2n                             p≤2n i<logp 2n

since if n < pi+1 then 2n/pi+1 mod 2 = 1. So we may conclude
                                                                                                   
theorem le Psi BPsi: ∀n. Psi(2∗n) ≤ B(2∗n)∗Psi n.
                                                                                                   
In particular, for any n
                                       Ψ(2n) ≤ 22n−1 Ψ(n)                                    (12)
and for 4 < n
                                       Ψ(2n) ≤ 22n−2 Ψ(n)                                    (13)
We may now use inductively these estimates to prove
                                                                                                   
theorem le Psi exp: ∀n. Psi(n) ≤ 2ˆ((2 ∗ n) −3).
                                                                                                   
For the proof, we need the monotonicity of Ψ, that is easily proved:
                 Y            Y                Y
        Ψ(n) =      plogp n ≤   plogp (n+1) ≤       plogp (n+1) = Ψ(n + 1)                   (14)
                    p≤n               p≤n                   p≤n+1

Then we check that the property holds for any n ≤ 8, which can be done by direct
computation. If n is larger than 8 we distinguish two cases, according to n is even
or odd. We only consider the case n = 2m + 1 that is the most interesting one.
Observe first that 8 < 2m + 1 implies 4 < m. Then we have:
                                      Ψ(n) = Ψ(2m + 1)
                                              ≤ Ψ(2m + 2)
                                              ≤ 22m Ψ(m + 1)
                                              ≤ 22m 22(m+1)−3
                                              ≤ 22(2m+1)−3
Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
5     BERTRAND’S POSTULATE                                                                          49

In conclusion, we have
                       2n/2 ≤ Ψ(n) ≤ nπ(n) ≤ Ψ(n)2 ≤ 24n−6 ≤ 24n                                 (15)

5.    BERTRAND’S POSTULATE
Our approach to Chebyshev’s theorem, as most modern presentations of the sub-
ject, essentially follows Chebyshev’s original idea, but in a rudimentary form which
provides a result that is numerically less precise, though of a similar nature. In
particular, Chebyshev was able to prove the asymptotic estimates
                                n                          n
                  (c1 + o(1))       ≤ π(n) ≤ (c2 + o(1))           (n → ∞)
                              log n                      log n
with
                         c1 = log(21/2 31/3 51/5 30−1/30 ) ≈ 0.92129
                         c2 = 6/5c1 ≈ 1.10555
In particular, since c2 < 2c1 , this implies that
                                           π(2n) > π(n)
for all large n. Actually, by direct computation, Chebyshev proved that the in-
equality remains true for all n, confirming for the first time Bertrand’s postulate.
   With our rough estimates, we could only prove the existence of a prime number
between n and 8n, for n sufficiently large. There exists however an alternative
approach to the proof of Bertrand’s postulate due to Erdös [10] (see also [13],
p. 344) that is well suited to a formal encoding in arithmetics1 .
5.1    Bertrand’s predicate
Let us define the following Bertands’ predicate:
                                                                                                         
definition bertrand :=λn. ∃p.n < p ∧ p ≤ 2∗n ∧ prime p.
                                                                                      
Bertrand’s postulate is the conjecture that the previous predicate holds for any
natural number n.
   Erdös proof is essentially a proof by contradiction; supposing the predicate to be
false, he derives an absurdity. The negation of Bertrand’s predicate is
                                                                                      
definition not bertrand :=λn.∀p.n < p → p ≤ 2∗n → ¬ (prime p).
                                                                                    
Since the quantification is bound, the predicate is decidable, that means that, even
in a system like Matita which has a constructive nature, you can prove
                                                                                    
theorem not not bertrand to bertrand: ∀n. ¬ (not bertrand n) → bertrand n.
                                                                                                         

1 Erdösargument was already exploited by Théry in his proof of Bertrand postulate [21]; however
he failed to provide a fully arithmetical proof, being forced to make use of the (classical, axiomatic)
library of Coq reals to solve the remaining inequalities.
50     ·     A. Asperti and W. Ricciotti

5.2   Chebyshev’s θ function
In order to use Erdös argument we need to introduce another important function
introduced by Chebyshev and largely used in analytic number theory [1]: the so
called theta-function.
   In particular, we shall work with the following variant (as for the Ψ function,
Chebyshev’s function is the naperian logarithm of our function)
                                Q
                                                                                   
definition theta: nat → nat :=λn.           {p < S n| primeb p} p.
                                                                                  
It is clear that for any n, θ(n) ≤ Ψ(n), so our upper bound for Ψ is also an upper
bound for θ. Since however providing an upper bound for θ(n) is much simpler, we
recall this direct argument here.
Let us split θ(2n + 1) in two parts:
                                                                                  
theorem
   Q    theta split: ∀m. theta (S (2∗m))
= ( {p ∈[S(S m)),S (S (2∗m))[ | primeb p} p)∗theta (S m).
                                                                                          
                                                                                 (2m+1)!
Let us now consider the following binomial coefficient M (m) =       (2m+1
                                                                       m )   =
                                                                                  m!m!    
definition M :=λm.bc (S(2∗m)) m.
                                                                                          
Using the binomial law, it is not difficult to prove that
                                                                                          
theorem lt M: ∀m. O < m → M m < 2ˆ(2∗m).
                                                                               
Every prime p between m + 2 and 2m + 1 must be a divisor of (2m + 1)! and hence
of M (m), so
                                                                               
theorem
  Q       divides pi p M: ∀m.
     {p ∈[S(S m)),S (S (2∗m))[ | primeb p} p | (M m).
qed.
                                                                                          
As a corollary,
                                                                                          
theorem
  Q      le pi p M: ∀m.
    {p ∈[S(S m)),S (S (2∗m))[ | primeb p} p ≤ (M m).
                                                                                          
and also
                                                                                          
theorem le theta M theta: ∀m.
  theta (S(2∗m)) ≤ (M m)∗theta (S m).
                                                                                          
Let us also observe that, since a prime larger than 2 cannot be even,
                                                                                          
theorem theta pred: ∀n. 1 < n → theta (2∗n) = theta (pred (2∗n)).
                                                                                          
We are now ready to prove the following statement:
                                                                                          
theorem le theta: ∀m.theta m ≤ 2ˆ(2∗m).
                                                                                       
The proof is by (generalized) induction on m. Let us suppose the statement is true
for any n < m, and let us prove it for m. Either m is even or it is odd (the two
cases are similar, and we only consider the first one (the other case is similar, using
theorem theta_pred). Let us suppose m = 2a + 1. Then
                θ(2a + 1) ≤ (M a) ∗ theta(Sa) ≤ 22a · 22(a+1) = 22(2a+1)
Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
5     BERTRAND’S POSTULATE                                                                  51

5.3    Erdös argument
Let
                                              X
                              k(n, p) =                (n/pi+1     mod 2)
                                            i<logp n

Then, B can also be written as
                                                   Y
                                          B(n) =         pk(n,p)
                                                   p≤n

We now split this product in two parts B1 and B2 , according to k(n, p) = 1 or
k(n, p) > 1.
                  P
                                                                               
definition k :=λn,p.        {i < log p n}((n/(pˆ(S i))\mod 2)).
                       Q
definition Bk :=λn.         {p < S n | primeb p}(pˆ(k n p)).

theorem eq B Bk: ∀n. B n = Bk n.
                       Q
definition B1 :=λn.        {p < S n | primeb p}(pˆ(leb (k n p) 1)∗ (k n p)).
                       Q
definition B2 :=λn.        {p < S n | primeb p}(pˆ(leb 2 (k n p))∗ (k n p)).

theorem eq Bk B1 B2: ∀n. Bk n = B1 n ∗ B2 n.
                                                                                                 
   Suppose that Bertrand postulate is f alse, hence there is no prime between n and
2n. Moreover, if 2n
                  3 < p ≤ n, then 2n/p = 2 and for i > 1 and n ≥ 6 2n/p = 0
                                                                              i

since
                                       2
                                         2n
                               2n ≤            ≤ pi
                                          3
so k(2n, p) = 0. Summing up, under the assumption that Bertrand postulate is
false,
                      Y           Y
            B1 (2n) =     p =          p ≤ θ(2n/3) ≤ 22(2n/3)          (16)
                             p ≤ 2n            p≤2n/3
                           k(2n, p) = 1
                                                                                                 
le B1 theta:∀n.6 ≤ n → not bertrand n → B1 (2∗n) ≤ theta (2 ∗ n / 3).
                                                                                                 
  On the other side, note that k(n, p) ≤ logp n, so if k(2n, p) ≥ 2 we also have
                            √
logp 2n ≥ 2 that implies p ≤ 2n. So
                                 Y                            Y                  √
              B2 (2n) =               pk(2n,p) ≤                   2n = (2n)π(       2n)
                                                                                           (17)
                                                              √
                               p ≤ 2n                     p≤ 2n
                             2 ≤ k(2n, p)

For n ≥ 15, π(n) ≤ n/2 − 1. Hence, for any n ≥ 27 > 152 , we have
                                                          √
                                                              2n/2−1
                                     B2 (2n) ≤ (2n)
Formally:
52     ·     A. Asperti and W. Ricciotti

                                                                                        
theorem le B2 exp: ∀n. 2ˆ7 ≤ n → B2 (2∗n) ≤ (2∗n)ˆ(pred(sqrt(2∗n)/2)).
                                                                                    
Putting everything together, supposing Bertrand’s postulate is false, we would have,
for any n ≥ 27
                                   22n ≤ 2nB(2n)
                                        = 2nB1 (2n)B2 (2n)
                                                            √
                                        ≤ 22(2n/3) (2n)         2n/2


Observe that
                                      22n = 22(2n/3) 22n/3
so, by cancellation,
                                                       √
                                       22n/3 ≤ (2n)        2n/2


and taking logarithms
                                           √
                                    2n       2n
                                       ≤        (log(2n) + 1)
                                     3       2
                                                                                        
theorem not bertrand to le2:
  ∀n.2ˆ7 ≤ n → not bertrand n → 2∗n / 3 ≤ (sqrt(2∗n)/2)∗S(log 2 (2∗n)).
                                                                                         
We want to find an integer m such that for all values larger than m the previous
equation is false; moreover, the integer m must be sufficiently small to allow to
check the remaining cases automatically in a feasible time. The trouble is that, in
our case, all operations are discrete, and it is not so easy to reason about inequalities
in arithmetics.
We must prove
                                √
                                  2n                    2n
                                     (log(2n) + 1) <
                                  2                      3
The strict inequality is the first source of trouble, so we prove instead
                                √
                                  2n                    2n
                                     (log(2n) + 1) ≤
                                  2                      4
using the fact that
                                         n        n
                                               <
                                       m+1        m
for any n ≥ m2 (in our case, n ≥ 8). By means of simple manipulations, it is easy
to transform the last equation in the following simpler form
                                                √
                              2(log(2n) + 1) ≤ 2n
or equivalently
                                        2(log n + 2)2 ≤ n
We now use the fact that for any a > 0 and any n ≥ 4a
                                            2a n2 ≤ 2n
Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
5     BERTRAND’S POSTULATE                                                             53

to get, for any n ≥ 28
                    2(log n + 2)2 ≤ 4(log n)2 = 22 (log n)2 ≤ 2log n ≤ n
In conlcusion, we are able to prove
                                                                                            
lemma sqrt bound: ∀n. 2ˆ8 ≤ n → 2∗(S(log 2 (2∗n))) ≤ sqrt (2∗n).
                                                                                            
and hence, as a simple corollary
                                                                                            
theorem bertrand up: ∀n. 2ˆ8 ≤ n → bertrand n.
                                                                                            

5.4    Automatic check
To complete the proof, we have still to check that Bertrand’s postulate remains
true for all integers less then 28 . This is very simple in principle: it is sufficient to
(1) generate the list of all primes up to the first prime larger than 28 (in reverse
    order)
(2) check that for any pair pi , pi+1 of consecutive primes in such list, pi < 2pi+1
Both the generation of the list and its check can be performed automatically. All
we have to do is to prove that our algorithm for generating primes is correct and
complete, and that the previous check is equivalent to Bertrand’s postulate, on the
given interval.
  With respect to the version discussed in [3], this part of the proof has been
completely rewritten and substantially simplified.
5.5    The list of primes
To compute the list of prime numbers, we use the following simple algorithm. We
first define a function list_divides l n that returns true if l contains at least a
divisor of n and false otherwise.
                                                                                   
let rec list divides l n :=
  match l with
  [ nil ⇒ false
  | cons (m:nat) (tl : list nat) ⇒ orb (dividesb m n) ( list divides tl n) ].
                                                                                            
                                                                                            
let rec lprim m i acc :=
  match m with
   [ O ⇒ acc
   | S m1 ⇒ match (list divides acc i) with
     [ true ⇒ lprim m1 (S i) acc
     | false ⇒ lprim m1 (S i) (acc@[i]) ]].

definition list of primes :=λn. lprim n 2 [].
                                                                                            
    For instance,
                                                                                            
example lprim ex: lprim 8 2 [ ] = [2; 3 ; 5 ; 7 ]. // qed.
                                                                                            
   Let us define a predicate primes_below l n stating that the list l is the list of
all primes strictly below n.
54     ·     A. Asperti and W. Ricciotti

                                                                                    
definition all primes :=λl.∀p. mem nat p l → prime p.
definition all below :=λl,n.∀p. mem nat p l → p < n.
definition primes all :=λl,n. ∀p. prime p → p < n → mem nat p l.

definition primes below :=λl,n. all primes l ∧ all below l n ∧ primes all l n.
                                                                                    
Then, by the definition of prime number, it is easy to prove that
                                                                                    
lemma ld to prime: ∀i,acc. 1 < i →
  primes below acc i → list divides acc i = false → prime i.
                                                                             
Using the previous property we can then prove the main invariant of the lprim
function, namely:
                                                                             
lemma lprim invariant: ∀n,i,acc. 1 < i →
  primes below acc i → primes below (lprim n i acc) (n+i).
                                                                                    
Since moreover
                                                                                    
lemma primes below2: primes below [] 2.
                                                                                    
we obtain
                                                                                    
lemma primes below lop: ∀n. primes below (list of primes n) (n+2).
                                                                                    

5.6   Checking
We perform the following test on the list:
                                                                                    
let rec checker l :=
  match l with
  [ nil ⇒ true
  | cons hd tl ⇒ match tl with
       [ nil ⇒ true
       | cons hd1 tl1 ⇒ leb (S hd) hd1 ∧ leb hd1 (2∗hd) ∧ checker tl
     ]
  ].
                                                                                   
Then, working by induction on the list, it is easy to prove the following property:
                                                                                   
theorem checker spec: ∀tl,a,l. checker l = true → l = a:: tl →
  ∀p. mem ? p tl → ∃pp. mem nat pp l ∧ pp < p ∧ p ≤ 2∗pp.
                                                                                   
  The last step consists in proving that the previous condition is enough to entail
Bertrand’s property for all n below the maximum prime in the list:
                                                                                   
theorem primes below to bertrand:
∀pm,l.prime pm → primes below l (S pm) →
  (∀p. mem ? p l → 2 < p → ∃pp. mem ? pp l ∧ pp < p ∧ p ≤ 2∗pp)
    → ∀n.0 < n → n < pm → bertrand n.
                                                                                    
  Finally we have just to compute the list of primes below 28 + 1 (that is prime),
and apply the previous results to conclude
Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
6    CONCLUSIONS                                                                     55

                                                                                          
lemma bertrand down : ∀n.O < n → n ≤ 2ˆ8 → bertrand n.
                                                                                          
The generation of the list of primes and its check takes less than 5 seconds.
Putting together this result with theorem bertrand_up, we finally get
                                                                                          
theorem bertrand : ∀n.O < n → bertrand n.
                                                                                          

6.   CONCLUSIONS
In this paper we presented the formalization, in the Matita interactive theorem
prover, of some results about Chebyshev’s functions ψ and θ, comprising a proof of
Bertrand’s postulate following the approach of Erdös [10]. The subject, even from
the point of view of formalization, is not completely original (see e.g. [21, 18]). For
us, it was mostly an opportunity to present and discuss the many novelties recently
introduced in Matita, comparing the old development relative to version 0.5.2 of
the system [5] and described in [3], with the current development relative to version
0.99 of the system.
   While porting it to the new version of the system, the arithmetical library has
undergone a deep revisitation, integration and restructuring, comprising e.g. the
new library of big operators discussed in section 2.
   The table in Figure 2 makes a comparison between the two versions of the proof:
for each file the first dimension is the number of lines, while the second one is the
number of theorems.
                     file                 Matita 0.5.2     Matita 0.99
                     logarithms            413    (20)     223     (21)
                     square root           217    (13)     221     (19)
                     binomial coeff.       259     (9)     192     (12)
                     order of primes       656    (33)     411     (37)
                     big operators         978    (30)     425     (27)
                     sigma and pi          526    (26)     188      (9)
                     factorial             325    (14)     145     (12)
                     chebyshev’s theta     486    (13)     213     (13)
                     chebishev’s psi       294    (11)     143     (13)
                     factorization         927    (25)     629     (32)
                     psi bounds           1123    (37)     507     (30)
                     bertrand (up)         683    (18)     446     (27)
                     bertrand (down)       526    (22)     240     (19)
                     total                7413   (271)    3983   (271)


                             Fig. 1.   Size of the developments


   In passing from version 0.5.2 to version 0.99 the size of the development has been
essentially reduced to one half, passing from an average of 28 lines per theorem to
less than 15.
   This is essentially due to two factors: the first one is the new compact syntax for
tactics, in the spirit of the SSReflect language [12]; the second one is the support for
small scale automation [7, 6] that relieves the user from spelling out a lot of trivial
steps. The difference can be appreciated by the following table, summarizing the
56     ·     REFERENCES

number of invocations of the most frequent tactics in the two versions of the above
files.
                                           Matita 0.5.2         Matita 0.99
                     tactic                    name     no.      name      no.
                     application               apply  2203          @     1792
                                        assumption      779
                     rewriting               rewrite  1110       </>      984
                                         reflexivity    244
                     simplification        simplify     255   normalize    122
                                                                   whd      76
                     introduction       intro/intros   435            #   1904
                     elimination               cases   306        cases    190
                                                elim   131         elim     92
                                                                      *     62
                     cut                        cut     89          cut    148
                     automation                auto     10           //    943


                              Fig. 2.    Number of tactics invocations


The 943 invocations of the auto tactic in version 0.99 not only replace the 779
invocations of “assumption” and the 244 invocations of “reflexivity”, but are also
responsible of the sensible reduction in the number of applications and rewritings.
The increase in the number of invocations of the introduction tactic is merely due
to the fact that the old tactic performed multiple introductions, delegating to the
system the choice of names, while the new tactic is nominal, and handles a single
variable at a time.
  In Hardy’s book [13], the proof of Bertrand’s postulate takes 42 lines, while
Chebyshev’s theorem takes precisely three pages (90 lines). With the new version
of the proof, this gives a de Brujin factor between 8 and 10, that is in line with
other formalization case studies in the realm of arithmetics [8, 15, 14].

References
 [1] T. M. Apostol. Introduction to Analytic Number Theory. Springer Verlag,
     1976.
 [2] Andrea Asperti and Cristian Armentano. A page in number theory. Journal
     of Formalized Reasoning, 1:1–23, 2008.
 [3] Andrea Asperti and Wilmer Ricciotti. About the formalization of some results
     by Chebyshev in number theory. In Proc. of TYPES’08, volume 5497 of LNCS,
     pages 19–31. Springer-Verlag, 2009.
 [4] Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi.
     Hints in unification. In Stefan Berghofer, Tobias Nipkow, Christian Urban,
     and Makarius Wenzel, editors, TPHOLs, volume 5674 of Lecture Notes in
     Computer Science, pages 84–98. Springer, 2009.
 [5] Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi.
     The Matita interactive theorem prover. In Proceedings of the 23rd International
     Conference on Automated Deduction (CADE-2011), Wroclaw, Poland, volume
     6803 of LNCS, 2011.
Journal of Formalized Reasoning Vol. 5, No. 1, 2012.
REFERENCES                                                                       57

 [6] Andrea Asperti and Enrico Tassi. Smart matching. In Intelligent Com-
     puter Mathematics, 10th International Conference, AISC 2010, 17th Sympo-
     sium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris,
     France, July 5-10, 2010. Proceedings, volume 6167 of Lecture Notes in Com-
     puter Science, pages 263–277. Springer, 2010.
 [7] Andrea Asperti and Enrico Tassi. Superposition as a logical glue. EPTCS,
     53:1–15, 2011.
 [8] Jeremy Avigad, Kevin Donnelly, David Gray, and Paul Raff. A formally verified
     proof of the prime number theorem. ACM Trans. Comput. Log., 9(1), 2007.
 [9] Yves Bertot, Georges Gonthier, Sidi Ould Biha, and Ioana Pasca. Canonical
     big operators. In TPHOLs, pages 86–101, 2008.
[10] P .Erdös. Beweis eines satzes von tschebyschef. Acta Scientifica Mathematica,
     5:194–198, 1932.
[11] Santiago Escobar, José Meseguer, and Prasanna Thati. Narrowing and rewrit-
     ing logic: from foundations to applications. Electr. Notes Theor. Comput. Sci.,
     177:5–33, 2007.
[12] Georges Gonthier and Assia Mahboubi. An introduction to small scale reflec-
     tion in coq. Journal of Formalized Reasoning, 3(2):95–152, 2010.
[13] G. H. Hardy. An introduction to the theory of numbers. Oxford University
     Press, 1938.
[14] John Harrison. A formalized proof of dirichlet’s theorem on primes in arith-
     metic progression. Journal of Formalized Reasoning, 2:63–83, 2009.
[15] John Harrison. Formalizing an analytic proof of the prime number theorem.
     J. Autom. Reasoning, 43(3):243–261, 2009.
[16] G. J. O. Jameson. The Prime Number Theorem, volume 53 of London Math-
     ematical Society Student Texts. Cambridge University Press, 2003.
[17] Srinivasa Ramanujan. A proof of bertrand’s postulate. Journal of the Indian
     Mathematical Society, 11:181–182, 1919.
[18] Riccardi. Pocklington’s theorem and bertrand’s postulate. Formalized Mathe-
     matics, 14(2):47–52, 2006.
[19] Claudio Sacerdoti Coen and Enrico Tassi. Nonuniform coercions via unification
     hints. volume 53 of EPTCS, pages 16–29, 2011.
[20] G. Tenenbaum and M. Mendès France. The Prime Numbers and Their Dis-
     tribution. American Mathematical Society, 2000.
[21] Laurent Théry. Proving pearl: Knuth’s algorithm for prime numbers. In
     Proceedings of TPHOLs’03, LNCS, pages 304–318. Springer Verlag, 2003.
