Assia Mahboubi
email: assia.mahboubi@inria.fr

Thomas Sibut-Pinote
email: thomas.sibut-pinote@ens-lyon.org

A FORMAL PROOF OF THE IRRATIONALITY OF ζ(3)

Keywords: formal proof, number theory, irrationality, creative telescoping, symbolic computation, Coq, Apéry's recurrences, Riemann zeta function

This paper presents a complete formal verification of a proof that the evaluation of the Riemann zeta function at 3 is irrational, using the Coq proof assistant. This result was first presented by Apéry in 1978, and the proof we have formalized essentially follows the path of his original presentation. The crux of this proof is to establish that some sequences satisfy a common recurrence. We formally prove this result by an a posteriori verification of calculations performed by computer algebra algorithms in a Maple session. The rest of the proof combines arithmetical ingredients and asymptotic analysis, which we conduct by extending the Mathematical Components libraries.

Theorem 1.1 (Apéry, 1978). The constant ζ(3) is irrational.

Introduction

In 1978, Apéry proved that ζ(3), which is the sum ∞ i=1 1 i 3 now known as the Apéry constant, is irrational. This result was the first dent in the problem of the irrationality of the evaluation of the Riemann zeta function at odd positive integers. As of today, this problem remains a long-standing challenge of number theory. Zudilin [START_REF] Zudilin | One of the numbers ζ(5), ζ(7), ζ(9), ζ(11) is irrational[END_REF] showed that at least one of the numbers ζ(5),ζ(7),ζ(9), ζ(11) must be irrational. Ball and Rivoal [START_REF] Rivoal | La fonction zêta de Riemann prend une infinité de valeurs irrationnelles aux entiers impairs[END_REF][START_REF] Ball | Irrationalité d'une infinité de valeurs de la fonction zêta aux entiers impairs[END_REF] established that there are infinitely many irrational odd zeta values. Fischler, Sprang and Zudilin proved [START_REF] Fischler | Many odd zeta values are irrational[END_REF] that there are asymptotically more than any power of log(s) irrational values of the Riemann zeta function at odd integers between 3 and s. But today ζ(3) is the only known such value to be irrational.

Van der Poorten reports [vdP79] that Apéry's announcement of this result was at first met with wide skepticism. His obscure presentation featured "a sequence of unlikely assertions" without proofs, not the least of which was an enigmatic recurrence (Lemma 3.3) satisfied by two sequences a and b. It took two months of collaboration between Cohen, Lenstra, and Van der Poorten, with the help of Zagier, to obtain a thorough proof of Apéry's theorem:

In the present paper, we describe a formal proof of this theorem inside the Coq proof assistant [START_REF]The Coq Proof Assistant[END_REF], using the Mathematical Components libraries [coq19]. This formalization follows the structure of Apéry's original proof. However, we replace the manual verification of recurrence relations by an automatic discovery of these equations, using symbolic computation. For this purpose, we use Maple packages to perform calculations outside the proof assistant, and we verify a posteriori the resulting claims inside Coq. By combining these verified results with additional formal developments, we obtain a complete formal proof of Theorem 1.1, formalized using the Coq proof assistant without additional axiom. In particular, the proof is entirely constructive, and does not rely on the axiomatic definition of real numbers provided in Coq's standard library. A previous paper [START_REF] Chyzak | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)[END_REF] reported on the implementation of the cooperation between a computer algebra system and a proof assistant used in the formalization. The present paper is self-contained: it includes a summary of the latter report, and provides more details about the rest of the formal proof. In particular, it describes the formalization of an upper bound on the asymptotic behavior of lcm(1, ..., n), the least common multiple of the integers from 1 to n, a part of the proof which was missing in the previous report.

The rest of the paper is organized as follows. We first describe the background formal theories used in our development (Section 2). We then outline the proof of Theorem 1.1 (Section 3). We summarize the algorithms used in the Maple session, the data this session produces and the way this data can be used in formal proofs (Section 4). We then describe the proof of the consequences of Apéry's recurrence (Section 5). Finally, we present an elementary proof of the bound on the asymptotic behavior of the sequence lcm(1, ..., n), which is used in this irrationality proof (Section 6), before commenting on related work and concluding (Section 7).

The companion code to the present article can be found in the following repository: https://github.com/math-comp/apery.

Preliminaries

This section provides some hints about the representation of the different natures of numbers at stake in this proof in the libraries backing our formal development. It also describes a few extensions we devised for these libraries and sets some notations used throughout this paper. Most of the material presented here is related to the Mathematical Components libraries [coq19, GAA + 13].

2.1. Integers. In Coq, the set N of natural numbers is usually represented by the type nat:

Inductive nat := O | S : nat → nat.
This type is defined in a prelude library, which is automatically imported by any Coq session. It models the elements of N using a unary representation: Coq's parser reads the number 2 as the term S (S O). The structural induction principle associated with this inductive type coincides with the usual recurrence scheme on natural numbers. This is convenient for defining elementary functions on natural numbers, like comparison or arithmetical operations, and for developing their associated theory. However, the resulting programs are usually very naive and inefficient implementations, which should only be evaluated for the purpose of small scale computations.

The set Z of integers can be represented by gluing together two copies of type nat, which provides a signed unary representation of integers:

Inductive int : Set := Posz of nat | Negz of nat.

If the term n : nat represents the natural number n ∈ N, then the term (Posz n): int represents the integer n ∈ Z and the term (Negz n): int represents the integer -(n + 1) ∈ Z. In particular, the constructor Posz : nat → int implements the embedding of type nat into type int, which is invisible on paper because it is just the inclusion N ⊂ Z. In order to mimic the mathematical practice, the constant Posz is declared as a coercion, which means in particular that unless otherwise specified, this function is hidden from the terms displayed by Coq to the user (in the current goal, in answers to search queries, etc).

The Mathematical Components libraries provide formal definitions of a few elementary concepts and results from number theory, defined on the type nat. For instance, they provide the theory of Euclidean division, a boolean primality test, the elementary properties of the factorial function, of binomial coefficients, etc. In the rest of the paper, we use the standard mathematical notations n! and n m for the corresponding formal definition of the factorial and of the binomial coefficients respectively. These libraries also define the p-adic valuation v p (n) of a number n: if p is a prime number, it is the exponent of p in the prime decomposition of n. However, we had to extend the available basic formal theory with a few extra standard results, like the formula giving the p-adic valuation of factorials: Lemma 2.1. For any n ∈ N and for any prime number p:

v p (n!) = log p n i=1 n p i .
Incidentally, the formal version of this formula is a typical example of the slight variations one may introduce in a mathematical statement, in order to come up with a formal sentence which is not only correct and faithful to the original mathematical result, but also a tool which is easy to use in subsequent formal proofs. First, although the fraction in the original statement of Lemma 2.1 may suggest that rational numbers play a role here, n m is in fact exactly the quotient of the Euclidean division of n by m. In the rest of the paper, for n, m ∈ N and m non-zero, we thus write n m for the quotient of the Euclidean division of n by m. Perhaps more interestingly, the formal statement of Lemma 2.1 rather corresponds to the following variant: For any prime p and any j, n ∈ N, such that n < p j+1 , v p (n!) =

j i=1 n p i .
Adding an extra variable to generalize the upper bound of the sum is a better option because it will ease unification when this formula is applied or used for rewriting. Moreover, we do not really need to introduce logarithms here: indeed, log p n is used to denote the largest power of p smaller than n. For this purpose, we could use the function trunc_log : nat → nat → nat provided by the Mathematical Components libraries, which computes the greatest exponent α such that n α ≤ m, in other words log n m . Better yet, since the summand is zero when the index i exceeds this value, we can simplify the side condition on the extra variable and require only that n < p j+1 .

The basic theory of binomial coefficients present in the Mathematical Components libraries describes their role in elementary enumerative combinatorics. However, when viewing binomial coefficients as a sequence which is a certain solution of a recurrence system, it becomes natural to extend their domain of definition to integers: we thus developed a small library about these generalized binomial coefficients. We also needed to extend these libraries with properties of multinomial coefficients. For n, k 1 , . . . , k l ∈ N, with

k 1 + • • • + k l = n, the coefficient of x k 1 1 • • • x k l l in the formal expansion of (x 1 + • • • + x l ) n is called a multinomial coefficient and denoted n k 1 ,...,k l . Its value is n! k 1 !...k l ! or equivalently, l i=1 k 1 +•••+k i k i
. The latter formula provides for free the fact that multinomial coefficients are non-negative integers and we use it in our formal definition: for (l : seq nat) a finite sequence l 1 , . . . , l s of natural numbers, then (multinomial l) is the multinomial coefficient l 1 +•••+ls l 1 ,...,ls :

Definition multinomial (l : seq nat) : nat := \prod_(0 ≤ i < size l) (binomial (\sum_(0 ≤ j < i.+1) l'_j) l'_i).

From this definition, we prove formally the other characterizations, as well as the generalized Newton formula describing the expansion of (x

1 + • • • + x l ) n .
2.2. Rational numbers, algebraic numbers, real numbers. In the Mathematical Components libraries, rational numbers are represented using a dependent pair. This type construct, also called Σ-type, is specific to dependent type theory: it makes possible to define a type that decorates a data with a proof that a certain property holds on this data. The Mathematical Components libraries also include a construction of the algebraic closure for countable fields, and thus a construction of Q, algebraic closure of Q, the field of rational numbers. The corresponding type, named algC is equipped with a structure of (partially) ordered, algebraically closed field [GAA + 13]. Slightly abusing notation, we denote by Q ∩ R the subset of Q containing elements with a zero imaginary part and we call such elements real algebraic numbers. Almost all the irrational numbers involved in the present proof are real algebraic numbers, and more precisely, they are of the form r 1 n for r a non-negative rational number r and for n ∈ N. The only place where these numbers play a role is in auxiliary lemmas for the proof of the asymptotic behavior of the sequence ( n ) n∈N , where n is the least common multiple of integers between 1 and n. They appear in inequalities expressing signs and estimations.

It might come as a surprise that we used the type algC of algebraic (complex) numbers to cast these quantities, although we do not actually need imaginary complex numbers. But this choice proved convenient due to the fact that the type algC features both a definition of n-th roots, and a clever choice of partial order. Indeed, although Q cannot be ordered as a field, it is equipped with a binary relation, denoted ≤, which coincides with the real order relation on

Q ∩ R: ∀x, y ∈ Q, x ≤ y ⇔ y -x ∈ R ≥0 .
In particular, for any z ∈ Q:

0 ≤ z ⇔ z ∈ R ≥0 and z ≤ 0 ⇔ z ∈ R ≤0 .
Moreover, the type algC is equipped with a function n.-root : algC → algC, defined for any (n : nat), such that (n.-root z) is the n-th (complex) root of z with minimal non-negative argument. Crucially, when (z : algC) represents a non-negative real number, (n.-root z) coincides with the definition of the real n-th root, and thus the following equivalence holds:

Vol. 17:1

A FORMAL PROOF OF THE IRRATIONALITY OF ζ(3) 16:5

The shape of Lemma rootC_ge0 is typical of the style pervasive in the Mathematical Components libraries, where equivalences between decidable statements are stated as boolean equalities. It expresses that for an algebraic number x, that is for x ∈ Q, we have x

1 n ∈ R ≥0 if and only if x ∈ R ≥0 .
The one notable place at which we need to resort to a larger subset of the real numbers is the definition of the number ζ(3), if only because as of today, it is not even known whether ζ(3) is algebraic or transcendental. This number is actually defined as the limit of the partial sums n m=1 1 m 3 , so we start our formal study by establishing the existence of this limit. More precisely, we show that this sequence of partial sums is a Cauchy sequence, with an explicit modulus of convergence.

Definition 2.2. A Cauchy sequence is a sequence (x n ) n∈N ∈ Q N together with a modulus of convergence m x : Q → N such that if ε is a positive rational number, then any two elements of index greater than m x (ε) are separated at most by ε.

Proposition 2.3. The sequence z n = n m=1 1 m 3 is a Cauchy sequence. Two sequences x and y are Cauchy equivalent if x and y are both Cauchy sequences, and if eventually |x n -y n | < ε, for any ε > 0. Real numbers could be constructed formally by introducing a quotient type, whose element are the equivalent classes of the latter relation. But this is rather irrelevant for this formalization, which involves explicit sequences and their asymptotic properties, rather than real numbers. For this reason, the formal statements in this formal proof only involve sequences of rational numbers, and a type of Cauchy sequences which pairs such a sequence with a proof that it has the Cauchy property. For instance, for two Cauchy sequences x and y, we write x < y if there is a rational number ε > 0 such that eventually x n + ε ≤ y n .

We benefited from the formal library about Cauchy sequences developed by Cohen [START_REF] Cohen | Construction of real algebraic numbers in Coq[END_REF]. This library defines Cauchy sequences of elements in a totally ordered field, and introduces a type (creal F) of Cauchy sequences over the totally ordered field F, given as a parameter. We thus use the instance (creal rat). The infix notation ==, in the notation scope CR, denotes the equivalence of Cauchy sequences, as in the statement (x == y)%CR, which states that the two Cauchy sequences x, y are equivalent. The library implements a setoid of field operations over this type [START_REF] Barthe | Setoids in type theory[END_REF][START_REF] Sozeau | A new look at generalized rewriting in type theory[END_REF], so as to facilitate substitutions for equivalents in formulas. In addition, the library provides a tactic called bigenough, which eases formal proofs by allowing a dose of laziness. This tactic is specially useful in proofs that a certain property on sequences is eventually true, which involve constructing effective moduli of convergence.

The formal statement corresponding to Theorem 1.1 is thus:

Theorem zeta_3_irrational : ~∃ (r : rat), (z3 == r%:CR)%CR.

where the postfix notation r%:CR denotes the Cauchy sequence whose elements are all equal to the rational number (r : rat). The term z3 is the Cauchy sequence corresponding to the partial sums (z n ) n∈N , that is, the dependent pair of this sequence with a proof of Property 2.3. The formal statement thus expresses that no constant rational sequence can be Cauchy equivalent to (z n ) n∈N . Interestingly, a long-lasting typo has marred the formal statement of theorem zeta_3_irrational in the corresponding Coq libraries, until writing the revised version of the present paper. Until then, the (inaccurate) statement was indeed:

Theorem incorrect_zeta_3_irrational : ~∃ (r : rat), (z3 = r%:CR)%CR.

Replacing == by = changes the statement completely, as it now expresses that there is no constant sequence of rationals equal to z3: and this is trivially true. The typo was already present in the version of the code that we made public for our previous report [START_REF] Chyzak | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)[END_REF], and the typo has remained unnoticed since. Yet fortunately, the proof script was right, and actually described a correct proof of the stronger statement zeta_3_irrational.

2.3. Notations. In this section, we provide a few hints on the notations used in the formal statements corresponding to the paper proof, so as to make precise the meaning of the statements we have proved formally. Indeed, this development makes heavy use of the notation facilities offered by the Coq proof assistant, so as to improve the readability of formulas. For instance, notation scopes allow to use the same infix notation for a relation on type nat, and in this case (x < y) unfolds to (ltn x y): bool, or for a relation on type creal rat), and in that case (x < y) unfolds to (lt_creal x y): Prop, the comparison predicate described in Section 2.2. Notation scopes can be made explicit using post-fixed tags: (x < y)%N is interpreted in the scope associated with natural numbers, and (x < y)%CR, in the scope associated with Cauchy sequences. Generic notations can also be shared thanks to type-class like mechanisms. The Mathematical Components libraries feature a hierarchy of algebraic structures [START_REF] Garillot | Packaging Mathematical Structures[END_REF], which organizes a corpus of theories and notations shared by all the instances of a same structure. This hierarchy implements inheritance and sharing using Coq's mechanisms of coercions and of canonical structures [START_REF] Mahboubi | Canonical Structures for the working Coq user[END_REF]. Each structure in the hierarchy is modeled by a dependent record, which packages a type with some operations on this type and with requirements on these operations. In order to equip a given type with a certain structure, one has to endow this type with enough operations and properties, following the signature prescribed by the structure. For example, these structures are all discrete, which means that they require a boolean equality test. In turn, all instances of all these structures share the same infix notation (x == y) for the latter boolean equality test between x and y: this notation makes sense for x,y in type nat,int, rat, alC, etc. because all these types are instances of the same structure. For instance, although type rat is a dependent pair (see Section 2.2), the boolean comparison test only needs to work with the data: by Hedberg's theorem [START_REF] Hedberg | A coherence theorem for Martin-Löf's type theory[END_REF], the proof stored in the proof component can be made irrelevant. Note that the situation is different for the type (creal rat) of Cauchy sequences. The formal statement of theorem zeta_3_irrational (see Section 2.2) uses the same == infix symbol, but in a different scope, in which it refers to Prop-valued Cauchy equivalence. Indeed, this relation cannot be turned constructively into a boolean predicate, as the comparison of Cauchy sequences is not effective. The type algC of algebraic numbers by contrast enjoys the generic version of the notation, as ordered fields only require a partial order relation.

Partial order, but also units of a ring, and inverse operations are examples of operations involved in some structures of the hierarchy, that make sense only on a subset of the elements of the carrier. In the dependent type theory implemented by Coq, it would be possible to use a dependent pair in order to model the source type of such an inverse operation. Instead, as a rule of thumb, the signature of a given structure avoids using rich types as the source types of their operations but rather "curry" the specification. For instance, the source type of the inverse operation in the structure of ring with units is the carrier type itself, but the signature of this structure also has a boolean predicate, which selects the units in this carrier type. The inverse operation has a default behavior outside units and the equations of the theory that involve inverses are typically guarded with invertibility conditions. Hence although the expression x^-1 * x is syntactically well-formed for any term x of an instance of ring with units, it can be rewritten to 1 only when x is known to be invertible.

The readability of formulas also requires dealing in a satisfactory manner with the inclusion of the various collections of numbers at stake, that are represented with distinct types, for instance:

N ⊂ Z ⊂ Q ⊂ Q.
The implementation of the inclusion N ⊂ Z was mentioned in Section 2.1. The canonical embedding of type int is available in the generic theory of rings, but unfortunately, it cannot be declared as a coercion, and eluded in formal statements: the type of the corresponding constant would violate the uniform inheritance condition prescribed by Coq's coercion mechanism [START_REF]The Coq Proof Assistant[END_REF]. Its formal definition hence comes with a generic postfix notation _%:~R, modeled as a reminiscence of the syntax of notation scopes and used to cast an integer as an element of another ring. The latter embedding is pervasive in formulas expressing the recurrence relations involved in this proof. Indeed, these recurrence relations feature polynomial coefficients in their indices and relate the rational elements of their solutions. See for instance Equation 3.2.

Computations. Using the unary representation of integers described in Section 2.1, the command:

Compute 100*1000.

which asks Coq to evaluate this product, triggers a stack overflow. For the purpose of running computations inside Coq's logic, on integers of a medium size, an alternate datastructure is required, together with less naive implementations of the arithmetical operations. The present formal proof requires this nature of computations at several places, for instance in order to evaluate sequences defined by a recurrence relation at a few particular values. For these computations, we used the binary representation of integers provided by the ZArith library included in the standard distribution of Coq, together with the fast reduction mechanism included in Coq's kernel [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF].

These two ingredients are also used behind the scene by tactics implementing verified decision procedures. For instance, we make extensive use of proof commands dedicated to the normalization of algebraic expressions like the field tactic for rational fractions, and the ring tactic for polynomials [START_REF] Grégoire | Proving equalities in a commutative ring done right in Coq[END_REF]. The field tactic generates proof obligations describing sufficient conditions for the simplifications it made. In our case, these conditions in turn are solved using the lia decision procedure for linear arithmetics [START_REF] Besson | Fast reflexive arithmetic tactics the linear case and beyond[END_REF].

These tactics work by first converting formulas in the goal into instances of appropriate data structures, suitable for larger scale computation. This pre-processing, hidden to the user, is performed by extra-logical code that is part of the internal implementation of these tactics. The situation is different when a computational step in a proof requires the evaluation of a formula at a given argument, and when both the formula and the argument are described using proof-oriented, inefficient representations. In that case, for instance for evaluating terms in a given sequence, we used the CoqEAL library [START_REF] Cohen | Refinements for Free! In Certified Programs and Proofs[END_REF], which provides an infrastructure automating the conversion between different data-structures and algorithms used to model the same mathematical objects, like different representations of integers or different implementations of a matrix product. Note that although the CoqEAL library itself depends on a library for big numbers, which provides direct access in Coq to Ocaml's library for arbitrary-precision, arbitrary-size signed integers, the present proof does not need this feature.

Outline of the proof

There exists several other proofs of Apéry's theorem. Notably, Beukers [START_REF] Beukers | A note on the irrationality of ζ(2) and ζ(3)[END_REF] published an elegant proof, based on integrals of pseudo-Lengendre polynomials, shortly after Apéry's announcement. According to Fischler's survey [START_REF] Fischler | Irrationalité de valeurs de zêta (d'après Apéry, Rivoal[END_REF], all these proofs share a common structure. They rely on the asymptotic behavior of the sequence n , the least common multiple of integers between 1 and n, and they proceed by exhibiting two sequences of rational numbers a n and b n , which have the following properties:

(1) For a sufficiently large n:

a n ∈ Z and 2 3 n b n ∈ Z; (2) The sequence δ n = a n ζ(3) -b n is such that: lim sup n→∞ |2δ n | 1 n ≤ ( √ 2 -1) 4 ;
(3) For an infinite number of values n, δ n = 0.

Altogether, these properties entail the irrationality of ζ(3). Indeed, if we suppose that there exists p, q ∈ Z such that ζ(3) = p q , then 2q 3 n δ n is an integer when n is large enough. One variant of the Prime Number theorem states that n = e n (1+o(1)) and since ( √ 2 -1) 4 e 3 < 1, the sequence 2q 3 n δ n has a zero limit, which contradicts the third property. Actually, the Prime Number theorem can be replaced by a weaker estimation of the asymptotic behavior of n , that can be obtained by more elementary means.

Lemma 3.1. Let n be the least common multiple of integers 1, . . . , n, then

n = O(3 n ).
Since we still have ( √ 2 -1) 4 3 3 < 1, this observation [START_REF] Hanson | On the product of the primes[END_REF][START_REF] Feng | A simple elementary proof for the inequality dn < 3 n[END_REF] is enough to conclude. Section 6 discusses the formal proof of Lemma 3.1, an ingredient which was missing at the time of writing the previous report on this work [START_REF] Chyzak | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)[END_REF].

In our formal proof, we consider the pair of sequences proposed by Apéry in his proof [START_REF] Apéry | Irrationalité de ζ(2) et ζ(3)[END_REF][START_REF] Van Der Poorten | A proof that Euler missed: Apéry's proof of the irrationality of ζ(3)[END_REF]:

a n = n k=0 n k 2 n+k k 2 , b n = a n z n + n k=1 k m=1 (-1) m+1 n k 2 n+k k 2 2m 3 n m n+m m (3.1)
where z n denotes n m=1 1 m 3 , as already used in Proposition 2.3. By definition, a n is a positive integer for any n ∈ N. The integrality of 2 3 n b n is not as straightforward, but rather easy to see as well: each summand in the double sum defining b n has a denominator that divides 2 3 n . Indeed, after a suitable re-organization in the expression of the summand, using standard properties of binomial coefficients, this follows easily from the following slightly less standard property:

Vol. 17:1

A FORMAL PROOF OF THE IRRATIONALITY OF ζ(3)

16:9

Proof. For i, j, n such that 1 ≤ j ≤ i ≤ n, the proof goes by showing that for any prime p, the p-adic valuation of j i j is at most that of n . Let us fix a prime number p. Let t p (i) be the largest integer e such that p e ≤ i. By definition, and since i ≤ n, we thus have p tp(i) | n and so t p (i) ≤ v p ( n ). Hence it suffices to prove that v p ( i j ) ≤ t p (i) -v p (j). Using Lemma 2.1, and because j ≤ i < p tp(i)+1 , we have:

v p ( i j ) = tp(i) k=1 i p k -( tp(i) k=1 j p k + tp(i) k=1 (i -j) p k ) Remember that for a, b ∈ N, a b is just a modulo b. Now for 1 ≤ k ≤ v p (j), and because p k |j, we have i p k = j p k + (i-j) p k
, and thus:

v p ( i j ) = tp(i) k=vp(j)+1 i p k -( tp(i) k=vp(j)+1 j p k + tp(i) k=vp(j)+1 (i -j) p k ) = tp(i)-vp(j) k=1 i p vp(j)+k -( tp(i)-vp(j) k=1 j p vp(j)+k + tp(i)-vp(j) k=1 (i -j) p vp(j)+k ) Now for any 1 ≤ k ≤ t p (i) -v p (j), we have: i p vp(j)+k ≤ j p vp(j)+k + (i -j) p vp(j)+k + 1
Summing both sides for k from 1 to t p (i) -v p (j) and using the previous identity for v p ( i j ) eventually proves that v p ( i j ) ≤ t p (i) -v p (j), which concludes the proof. The rest of the proof is a study of the sequence δ n = a n ζ(3) -b n . It not difficult to see that δ n tends to zero, from the formulas defining the sequences a and b, but we also need to prove that it does so fast enough to compensate for 3 n , while being positive. In his original proof, Apéry derived the latter facts by combining the definitions of the sequences a and b with the study of a mysterious recurrence relation. Indeed, he made the surprising claim that Lemma 3.3 holds: Lemma 3.3. For n ≥ 0, the sequences (a n ) n∈N and (b n ) n∈N satisfy the same second-order recurrence:

(n + 2) 3 y n+2 -(17n 2 + 51n + 39)(2n + 3)y n+1 + (n + 1) 3 y n = 0.

(3.2) Equation 3.2 is a typical example of a linear recurrence equation with polynomial coefficients and standard techniques [START_REF] Salvy | An Algolib-aided version of Apéry's proof of the irrationality of ζ(3)[END_REF][START_REF] Van Der Poorten | A proof that Euler missed: Apéry's proof of the irrationality of ζ(3)[END_REF] can be used to study the asymptotic behavior of its solutions. Using this recurrence and the initial conditions satisfied by a and b, one can thus obtain the two last properties of our criterion, and conclude with the irrationality of ζ(3). For the purpose of our formal proof, we devised an elementary version of this asymptotic study, mostly based on variations on the presentation of van der Poorten [vdP79]. We detail this part of the proof in Section 5.

Using only Equation 3.2, even with sufficiently many initial conditions, it would not be easy to obtain the first property of our criterion, about the integrality of a n and b n for a large enough n. In fact, it would also be difficult to prove that the sequence δ tends to zero: we would only know that it has a finite limit, and how fast the convergence is. By contrast, it is fairly easy to obtain these facts from the explicit closed forms given in Formula 3.1.

The proof of Lemma 3.3 was by far the most difficult part in Apéry's original exposition. In his report [vdP79], van der Poorten describes how he, with other colleagues, devoted significant efforts to this verification after having attended the talk in which Apéry exposed his result for the first time. Actually, the proof of Lemma 3.3 boils down to a routine calculation using the two auxiliary sequences U n,k and V n,k , themselves defined in terms of

λ n,k = n k 2 n+k k 2 (with λ n,k = 0 if k < 0 or k > n): U n,k = 4(2n + 1)(k(2k + 1) -(2n + 1) 2 )λ n,k , V n,k = U n,k n m=1 1 m 3 + k m=1 (-1) m-1 2m 3 n m n+m m + 5(2n + 1)k(-1) k-1 n(n + 1) n k n + k k
The key idea is to compute telescoping sums for U and V . For instance, we have:

U n,k -U n,k-1 = (n + 1) 3 λ n+1,k -(34n 3 + 51n 2 + 27n + 5)λ n,k + n 3 λ n-1,k (3.3)
Summing Equation 3.3 on k shows that the sequence a satisfies the recurrence relation of Lemma 3.3. A similar calculation proves the analogue for b, using telescoping sums of the sequence V . Not only is the statement of Formula 3.2 difficult to discover: even when this recurrence is given, finding the suitable auxiliary sequences U and V by hand is a difficult task. Moreover, there is no other known way of proving Lemma 3.3 than by exhibiting this nature of certificates. Fortunately, the sequences a and b belong in fact to a class of objects well known in the fields of combinatorics and of computer-algebra. Following seminal work of Zeilberger's [START_REF] Zeilberger | A holonomic systems approach to special functions identities[END_REF], algorithms have been designed and implemented in computer-algebra systems, which are able to obtain linear recurrences for these sequences. For instance the Maple package Mgfun (distributed as part of the Algolib [alg13] library) implements these algorithms, among others. Basing on this implementation, Salvy wrote a Maple worksheet [START_REF] Salvy | An Algolib-aided version of Apéry's proof of the irrationality of ζ(3)[END_REF] that follows Apéry's original method but interlaces Maple calculations with human-written parts. In particular, this worksheet illustrates how parts of this proof, including the discovery of Apéry's mysterious recurrence, can be performed by symbolic computations. Our formal proof of Lemma 3.3 follows an approach similar to the one of Salvy. It is based on calculations performed using the Algolib library, and certified a posteriori. This part of the formal proof is discussed in Section 4.1.

Algorithms, Recurrences and Formal Proofs

This section quotes and summarizes an earlier publication [START_REF] Chyzak | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)[END_REF], describing a joint work with Chyzak and Tassi.

Lemma 3.3 is the bottleneck in Apéry's proof. Both sums a n and b n in there are instances of parameterized summation: they follow the pattern F n = β(n) k=α(n) f n,k in which the summand f n,k , potentially the bounds, and thus the sum, depend on a parameter n. This makes it appealing to resort to the algorithmic paradigm of creative telescoping, which was developed for this situation in computer algebra. 16:11 4.1. Recurrences as a data structure for sequences. A fruitful idea from the realm of computer algebra is to represent sequences not explicitly, such as the univariate (n!) n or the bivariate ( n k ) n,k , but by a system of linear recurrences of which they are solutions such as {u n+1 = (n + 1)u n } or {u n+1,k = n+1 n+1-k u n,k , u n,k+1 = n-k k+1 u n,k }, accompanied with sufficient initial conditions. Sequences which can be represented in such a way are called ∂-finite. The finiteness property of their definition makes algorithmic most operations under which the class of ∂-finite sequences is stable.

In the specific bivariate case which interests us, let S n be the shift operator in n mapping a sequence (u n,k ) n,k to (u n+1,k ) n,k and similarly, let S k map (u n,k ) n,k to (u n,k+1 ) n,k . Linear recurrences canceling a sequence f can be seen as elements of a non-commutative ring of polynomials with coefficients in Q(n, k), and with the two indeterminates S n and S k , with the action (P • f ) n,k = (i,j)∈I p i,j (n, k)f n+i,k+j , where subscripts denote evaluation. For example for f n,k = n k , the previous recurrences once rewritten as equalities to zero can be represented as P • f = 0 for P = S n -n+1 n+1-k and P = S k -n-k k+1 , respectively. Computer algebra gives us algorithms to produce canceling operators for operations such as the addition or product of two ∂-finite sequences, using for both its inputs and output a Gröbner basis as a canonical way to represent the set of their canceling operators, which gives some uniqueness guarantees.

The case of summing a sequence (f n,k ) into a parameterized sum F n = n k=0 f n,k is more involved: it follows the method of creative telescoping [START_REF] Zeilberger | The method of creative telescoping[END_REF], in two stages. First, an algorithmic step determines pairs (P, Q) satisfying

P • f = (S k -1)Q • f (4.1)
with P ∈ Q(n)[S n ] and Q ∈ A. To continue with our example f n,k = n k , we could choose P = S n -2 and Q = S n -1. Second, a systematic but not fully algorithmic step follows: summing (4.1) for k between 0 and n + deg P yields

(P • F ) n = (Q • f ) k=n+deg P +1 -(Q • f ) k=0 .
(4.2) Continuing with our binomial example, summing (4.1) for k from 0 to n + 1 (and taking special values into account) yields n+1 k=0 n+1 k -2 n k=0 n k = 0, a special form of (4.2) with right-hand side canceling to zero. This tells us that the sequence ( n k=0 n k ) n∈N is a solution of the same recurrence P = S n -2 as (2 n ) n∈N : a simple check of initial values gives us the identity ∀n ∈ N, 2 n = n k=0 n k . The formula (4.2) in fact assumes several hypotheses that hold not so often in practice; this will be formalized by Equation (4.3) below. 4.2. Apéry's sequences are ∂-finite constructions. The sequences a and b in (3.1) are ∂-finite: they have been announced to be solutions of (3.2). But more precisely, they can be viewed as constructed from "atomic" sequences by operations under which the class of ∂-finite sequences is stable. This is summarized in Table 1.

In this table, Gröbner bases are systems of recurrence operators: at each line in the table, the sequence given in explicit form is a solution of the system of recurrences described by the operators in the Gröbner basis column. Note that in fact none of these results rely on the specific sequences in the explicit form: at each step, a new Gröbner basis is obtained from known ones, the ones that are cited in the input column. The table can also be read bottom-up for the purpose of verification: the Gröbner basis obtained at a given step can be verified using only the Gröbner bases obtained at some previous steps, all the way down to C and D. These operators describe a more general class of (germs of) sequences than step explicit form GB operation input(s)

1 c n,k = n k 2 n+k k 2 C direct 2 a n = n k=1 c n,k A creative telescoping C 3 d n,m = (-1) m+1 2m 3 ( n m )( n+m m ) D direct 4 s n,k = k m=1 d n,m S creative telescoping D 5 z n = n m=1 1 m 3 Z direct 6 u n,k = z n + s n,k U addition Z and S 7 v n,k = c n,k u n,k V product C and U 8 b n = n k=1 v n,k B creative telescoping V
Table 1: Construction of a n and b n : At each step, the Gröbner basis named in column GB, which annihilates the sequence given in explicit form, is obtained by the corresponding operation on ideals, with input(s) given on the last column.

just the explicit sequences used in this table, thus initial conditions are needed to describe a precise sequence.

4.3. Provisos and sound creative telescoping. We illustrate the process of verifying candidate new recurrences using known ones on the example of Pascal's triangle rule. One can "almost prove" Pascal's triangle rule using only the following recurrences, satisfied by binomial coefficients:

u n+1,k = n + 1 n + 1 -k u n,k and u n,k+1 = n -k k + 1 u n,k .
Indeed, we have:

n + 1 k + 1 - n k + 1 - n k = n + 1 n -k n -k k + 1 - n -k k + 1 -1 n k = 0 × n k = 0,
but this requires k = -1 and k = n. Therefore, this does not prove Pascal's rule for all n and k. The phenomenon is general: computer algebra is unable to take denominators into account. This incomplete modeling of sequences by algebraic objects may cast doubt on these computer-algebra proofs, in particular when it comes to the output of creative-telescoping algorithms. By contrast, in our formal proofs, we augmented the recurrences with provisos that restrict their applicability. In this setting, we validate a candidate identity like the Pascal triangle rule by a normalization modulo the elements of a Gröbner basis plus a verification that this normalization only involves legal instances of the recurrences. In the case of creative telescoping, Eq. (4.1) takes the form:

(n, k) / ∈ ∆ ⇒ (P • f ,k ) n = (Q • f ) n,k+1 -(Q • f ) n,k , (4.3)
where ∆ ⊂ Z 2 guards the relation and where f ,j denotes the univariate sequence obtained by specializing the second argument of f to j. Thus our formal analogue of Eq. (4.2) takes 16:13 this restriction into account and has the shape

(P • F ) n = (Q • f ) n,n+β+1 -(Q • f ) n,α + r i=1 i j=1 p i (n) f n+i,n+β+j + α≤k≤n+β ∧ (n,k)∈∆ (P • f ,k ) n -(Q • f ) n,k+1 + (Q • f ) n,k , (4.4)
for F the sequence with general term F n = n+β k=α f n,k and where P = r i=0 p i (n)S i n . The last term of the right-hand side, which we will call the singular part, witnesses the possible partial domain of validity of relation (4.3). Thus the operator P is a valid recurrence for the sequence F if the right-hand side of Eq. (4.4) normalizes to zero, at least outside of an algebraic locus that will guard the recurrence. 4.4. Generated Operators, hand-written provisos, and formal proofs. For each step in Table 1, we make use of the data computed by the Maple session in a systematic way, using pretty-printing code to express this data in Coq. As mentioned in Section 4.3, we manually annotate each operator produced by the computer-algebra program with provisos and turn it this way into a conditional recurrence predicate on sequences. In our formal proof, each step in Table 1 consists in proving that some conditional recurrences on a composed sequence can be proved from some conditional recurrences known for the arguments of the operation.

These steps are far from automatic, mainly because the singular part yields terms which have to be reduced manually through trial-and-error using a Gröbner basis of annihilators for f , but also because we have to show that some rational-function coefficients of the remaining instances of f are zero. This is done through a combination of the field and lia proof commands, helped by some factoring of denominators pre-obtained in Maple. 4.5. Composing closures and reducing the order of B. In order to complete the formal proof of Lemma 3.3, we verify formally that each sequence involved in the construction of a n and b n is a solution of the corresponding Gröbner system of annotated recurrence, starting from c n , d n , and z n all the way to the the final conclusions. This proves that a n is a solution of the recurrence (3.2) but only provides a recurrence of order four for b n . We then prove that b also satisfies the recurrence (3.2) using four evaluations b 0 , b 1 , b 2 , b 3 .

Consequences of Apéry's recurrence

In this section, we detail the elementary proofs of the properties obtained as corollaries of Lemma 3.3. We recall, from Section 3, that these properties describe the asymptotic behavior of the sequence δ n = a n ζ(3) -b n , with:

a n = n k=0 n k 2 n+k k 2 , b n = a n z n + n k=1 k m=1 (-1) m+1 n k 2 n+k k 2 2m 3 n m n+m m
(5.1)

Throughout the section, we use the vocabulary and notations of Cauchy sequences numbers, as introduced in Section 2.2. For instance, we have:

Lemma 5.1. For any ε, eventually |z n -bn an | < ε.

where b_over_a_seq n represents bn an . The notation {asympt e : i / P} , used in this formal statement, comes from the external library for Cauchy sequences [START_REF] Cohen | Construction of real algebraic numbers in Coq[END_REF]. In the expression {asympt e : i / P} , asympt is a keyword, and both e and i are names for variables bound in the term P. This expression unfolds to the term (asympt1 (fun e i => P)), a dependent pair that ensures the existence of an explicit witness that property P asymptotically holds: The formalization of Corollary 5.2 then comes in three steps: first the proof that ( bn an ) n∈N is a Cauchy sequence, as formalized by the creal_aiom predicate:

Corollary creal_b_over_a_seq : creal_axiom b_over_a_seq.
This formal proof is a one-liner, because the corresponding general argument, a sequence that is asymptotically close to a Cauchy sequence will itself satisfy the Cauchy property, is already present in the library. Then, the latter proof is used to forge an inhabitant of the type of rational Cauchy sequences, which just amounts to pairing the sequence b_over_a_seq : nat → rat with the latter proof:

Definition b_over_a : {creal rat} := CReal creal_b_over_a_seq. Now we can state the proof of equivalence between the two Cauchy sequences, i.e., between the two corresponding terms of type {creal rat} :

Fact z3_eq_b_over_a : (z3 == b_over_a)%CR.
The proof of the latter fact is again a one-liner, with no additional mathematical content added to lemma creal_b_over_a_seq, but it provides access to automation based on setoid rewriting facilities

The Mathematical Components libraries do not cover any topic of analysis, and even the most basic definitions of transcendental functions like the exponential or the logarithm are not available. However, it is possible to obtain the required properties of the sequence δ by very elementary means, and almost all these elementary proofs can be inferred from a careful reading and a combination of Salvy's proof [START_REF] Salvy | An Algolib-aided version of Apéry's proof of the irrationality of ζ(3)[END_REF] and of van der Poorten's description [vdP79].

Following van der Poorten, we introduce an auxiliary sequence (w n ) ∈ Q n , defined as:

w n = b n+1 a n+1 b n a n = b n+1 a n -a n+1 b n .
The sequence w is called a Casoratian: as a and b are solutions of a same linear recurrence relation (3.2) of order 2, this can be seen as a discrete analogue of the Wronskian for linear differential systems. For example, w satisfies a recurrence relation of order 1, which provides a closed form for w:

Lemma 5.3. For n ≥ 2, w n = 6 (n+1) 3 . 16:15

Proof. Since a and b satisfy the recurrence relation 3.1, w satisfies the relation:

∀k ∈ N, (k + 2) 3 w k+1 -(k + 1) 3 w k = 0.
The result follows from the computation of w 0 .

From this formula, we can obtain the positivity of the sequence δ, and an evaluation of its asymptotic behavior in terms of the sequence a.

Corollary 5.4. For any n ∈ N such that 2 ≤ n, 0 < ζ(3) -bn an . The formal statement corresponding to Corollary 5.4 is the following:

Lemma lt0_z3_minus_b_over_a (n : nat) : 2 ≤ n → (0%:CR < z3 -(b_over_a_seq n)%:CR)%CR.
Note the postfix CR tag which enforces that inside the corresponding parentheses, notations are interpreted in the scope associated with Cauchy sequences: in particular, the order relation (on Cauchy sequences) is the one described in Section 2.2.

Term (b_over_a_seq n : rat) is the rational number an bn , which is casted as a Cauchy real, the corresponding constant sequence, using the postfix %:CR, so as to be subtracted to the Cauchy sequence z3. This proof in particular benefits from setoid rewriting using equivalences like z3_eq_b_over_a, the formal counterpart of Corollary 5.2. Proof. Since ζ(3) = b a , it is sufficient to show that there exists a constant K, such that for

any k < l, b l a l -b k a k ≤ K a 2 k
. But since a is an increasing sequence, Lemma 5.3 proves that for

any k < l, b l a l -b k a k ≤ l-1 i=k w i a i a i+1 ≤ l-1 i=k 6 (i+1) 3 a 2 k ≤ K a 2 k , for any K greater than 6 • ζ(3).
The last remaining step of the proof is to show that the sequence a grows fast enough. The elementary version of Lemma 5.6 is based on a suggestion by F. Chyzak.

Lemma 5.6.

33 n = O(a n ).
Proof. Consider the auxiliary sequence ρ n = a n+1 an . Since ρ 51 is greater than 33, we only need to show that the sequence ρ is increasing. For the sake of readability, we denote µ n and ν n the fractions coefficients of the recurrence satisfied by a, obtained from Equation 3.2 after division by its leading coefficient. Thus a satisfies the recurrence relation:

a n+2 -µ n a n+1 + ν n = 0.
For n ∈ N, we also introduce the function h n (x) = µ n + νn x , so that ρ n+1 = h n (ρ n ). The polynomial P n (x) = x 2 -µ n x + ν n has two distinct roots x n < x n , and the formula describing the roots of polynomials of degree 2 show that 0 < x n < 1 < x n and that the sequence x n is increasing. But since h n (x) -x = -Pn(x)

x , for 1 < x < x n , we have h n (x) > x. A direct recurrence shows that for any n ≥ 2, ρ n ∈ [1, x n ], which concludes the proof.

In the formal proof of Lemma 5.6, the computation of ρ 51 was made possible by using the CoqEAL library, as already mentioned in Section 2.4. This proof also requires a few symbolic computations that are a bit tedious to perform by hand: in these cases, we used Maple as an oracle to massage algebraic expressions, before formally proving the correctness of the simplification. This was especially useful to study the roots x n and x n of P n .

We can now conclude with the limit of the sequence 3 n δ n , under the assumption that

n = O(3 n ). Corollary 5.7. lim n→∞ ( 3 n δ n ) = 0.
Proof. Immediate, since δ n = O( 1 an ) by Corollary 5.5, and 3 n = O((3 3 ) n ), and 3 3 < 33. In the next Section, we describe the proof of the last remaining assumption, about the asymptotic behavior of n .

6. Asymptotics of lcm(1, ..., n)

For any integer 1 ≤ n, let n denote the least common multiple lcm(1, ..., n) of the integers no greater than n. By convention, we set 0 = 1. The asymptotic behavior of the sequence ( n ) is a classical corollary of the Prime Number Theorem. A sufficient estimation for the present proof can actually but obtained as a direct consequence, using an elementary remark about the p-adic valuations of n . Remark 6.1. For any prime number p, the integer p vp( n) is the highest power of p not exceeding n, so that:

v p ( n ) = log p (n) .
Proof. Noticing that v p (lcm(a, b)) = max(v p (a), v p (b)), we see by induction on n that

v p ( n ) = n max i=1 v p (i).
Recall from Section 2.1 that log p (n) is a notation for the greatest integer α such that p α ≤ n. Since α = v p (p α ), we have α ≤ v p ( n ). Now suppose that v p ( n ) = v p (i) for some i ∈ {1, . . . , n}. Then i = p vp(i) q with gcd(p, q) = 1 so that

p vp( n) = p vp(i) ≤ i ≤ n and thus v p ( n ) ≤ α. This proves that v p ( n ) = α.
By Remark 6.1, n can hence be written as p≤n p log p (n) and therefore:

ln( n ) = p≤n ln(p log p (n) ) ≤ p≤n ln(n).
If π(n) is the number of prime numbers no greater than n, we hence have:

ln( n ) ≤ π(n) ln(n).
The Prime Number theorem states that π(n) ∼ n ln(n) ; we can thus conclude that:

n = O(e n ).
Note that this estimation is in fact rather precise, as in fact:

n ∼ e n (1+o(1)) .

Vol. 17:1 A FORMAL PROOF OF THE IRRATIONALITY OF ζ(3)

16:17

Although the standard proofs of this theorem use tools from complex analysis like contour integrals, their choice was guided by the corpus of formalized mathematics available for the Isabelle proof assistant, or the limits thereof. Although less direct, the proof by A. Selberg and P. Erdös is indeed more elementary and avoids complex analysis completely.

6.1. Statement, Notations and Outline. In order to prove Corollary 5.7 in Section 5, we only need to resort to Lemma 3.1, i.e., to the fact that:

n = O(3 n
). This part of the proof was left as an assumption in our previous report [START_REF] Chyzak | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)[END_REF]. This weaker description of the asymptotic behavior of ( n ) was in fact known before the first proofs of the Prime Number theorem but our formal proof is a variation on an elementary proof proposed by Hanson [START_REF] Hanson | On the product of the primes[END_REF].

The idea of the proof is to replace the study of n by that of another sequence C(n). The latter is defined as a multinomial coefficient depending on elements of a fast-growing sequence α. The fact that n i=1 α 1/α i i < 3 independently of n then allows to show that

C(n) = O(3 n ).
6.2. Proof. Define the sequence (α n ) n∈N by α 0 = 2, and

α n+1 = α 1 α 2 • • • α n + 1 for n ≥ 1. By an induction on n, this is equivalent to α n+1 = α 2 n -α n + 1. For n, k ∈ N, let C(n, k) = n! n/α 1 ! n/α 2 ! • • • n/α k ! .
As soon as α k ≥ n, C(n, k) is independent of k and we denote C(n) = C(n, k) for all such k.

Hanson directly defines C(n) as a limit, but we found this to be inconvenient to manipulate in the proof. Moreover, most inequalities stated on C(n) actually hold for C(n, k) with little or no more hypotheses. The following technical lemma will be useful in the study of this sequence.

Lemma 6.2. For k ∈ N,

k i=1 1 α i = α k+1 -2 α k+1 -1 < 1 and thus for x ∈ Q with x ≥ 1, x > k i=1 x α i .
Proof. The proof is done by induction and relies on the fact that if a ∈ Q and m ∈ N + , we have a m = a m .

Notice that by Lemma 6.2, k i=0 n α i < n and thus:

C(n, k) = k i=0 n α i n/α 1 , n/α 2 , . . . , n/α k n! k i=0 n α i ! .
In particular, C(n, k) ∈ N. The goal is now to show that n ≤ C(n) < K • 3 n for some K.

In the following, for n, k, p ∈ N and p prime, we denote β p (n, k) for v p (C(n, k)).

Lemma 6.3. For all n, k ∈ N, with 1 ≤ n and p prime,

β p (n, k) ≥ log p (n) = v p ( n ).
Therefore C(n, k) ≥ n for all n.

Proof. The proof uses Lemma 2.1.

β p (n, k) = v p (n!) - k i=1 v p ( n/α i !) = log p (n) i=1 n/p i - k i=1 log p ( n α i ) j=1 n α i p j = log p (n) i=1   n/p i - k j=1 n p i α j   ≥ log p (n) i=1 1 (because 1 α i < 1 by Lemma 6.2).
Since n = p≤n p log p (n) from Remark 6.1, we get n ≤ C(n, k) = p≤n p βp(n,k) .

Lemma 6.4. For i ≥ 1 and n ≥ α i ,

n α i n α i n α i n α i < 10 n α i α i -1 α i .
Proof. If n = α i , we have 1 < √ 10 ≤ 10 α i -1 α i , hence the result. Otherwise n > α i : let us write n = bα i + r, with 0 ≤ r < α i the Euclidean division of n by α i . We have:

n -α i + 1 α i = b -1 + r + 1 α i ≤ b. Since b = n α i , it follows that n-α i +1 α i ≤ n α i . Now for 1 2 ≤ x, the function x x is increasing, thus since 1 2 ≤ 1 α i ≤ n-α i +1 α i , we deduce that n-α i +1 α i n-α i +1 α i ≤ n α i n α i
, and we hence have:

n α i n α i n α i n α i ≤ n α i n α i n-α i +1 α i n-α i +1 α i = 1 + α i -1 n -α i + 1 n-α i +1 α i -1 α i -1 α i n α i α i -1 α i
.

The first operand in the last expression is of the shape 1 + 1 x x α i -1 α i , where x is a positive rational. We showed using only elementary properties of rational numbers, like the binomial formula or the summation formula for geometric progressions, that for any such positive rational number x, 1 + 1 x x < 10, hence the result. Note that we only needed that there exist a constant K > 0 such that 1 + 1 x x < K.

Of course, using elementary real analysis allows for the tighter bound e, which was used in Hanson's paper, but this bound is irrelevant for the final result. We can now establish the following bound on C(n, k): 16:19 Lemma 6.5. For k ≥ 1 and n ≥ 2,

C(n, k) < n n n α 1 n α 1 • • • n α k n α k . Proof. First observe that if m = m 1 + • • • + m k
where m and the m i are (not all zero) non-negative integers, we have because of the multinomial theorem:

(m 1 + • • • + m k ) m ≥ m m 1 , . . . , m k m m 1 1 • • • m m k k . (6.1)
Let k ≥ 1, and define:

t = k i=1 n α i .
Then t < n by Lemma 6.2. We have:

C(n, k) = n • (n -1) • • • (t + 1) t n/α 1 , n/α 2 , . . . , n/α k . (6.2)
Because of equation (6.1), we know that t n/α 1 , n/α 2 , . . . , n/α k ≤ t t n/α 1 n/α 1 n/α 2 n/α 2 . . . n/α k n/α k . (6.3)

From equations (6.2) and (6.3) we deduce that

C(n, k) < n n n/α 1 n/α 1 n/α 2 n/α 2 . . . n/α k n/α k . Lemma 6.6. Let k ≥ 3, n ∈ N. If α k ≤ n then k < log 2 log 2 n + 2.
Proof. First observe by a simple induction that for all k ≥ 3,

α k > 2 2 k-2 + 1 so that k -2 < log 2 ( log 2 α k ) ≤ log 2 ( log 2 n ) . Lemma 6.7. Let k ≥ 1, n ∈ N. If α k ≤ n, C(n, k) < n n ( 10 n α 1 ) α 1 -1 α 1 ( 10 n α 2 ) α 2 -1 α 2 . . . ( 10 n α k ) α k -1 α k 10 n α 1 10 n α 1 10 n α 1 10 n α 1 . . . 10 n α k 10 n α k .
Proof. The result is straightforward by combining Lemmas 6.4 and 6.5.

Lemma 6.8.

Let w k = k i=1 α 1 α i i , k ≥ 1.
Then w k is increasing and there exists w ∈ R, with w < 2.98, such that w k < w.

16:20

A. Mahboubi and T. Sibut-Pinote Vol. 17:1

Proof. The sequence w k is increasing because α i

1 α i > 1 (because α i > 1). Since α 2 i > α i+1 > (α i -1) 2 , one can see that for i ≥ 3, α 1 α i+1 i+1 < α 1 α i
i , so that for all k ≥ 1 and l ≥ 0,

w k+l ≤ k i=1 α 1 α i i • α 1 α k+1 l i=0 1 2 i k+1 ≤ w k • α 2 α k+1 k+1 .
We establish by an elementary external computation verified in Coq that α Remark 6.9. For k ≥ 1, we have

1 α 1 1 < 283 200 , α 1 α 2 2 < 1443 1000 , α 1 α 3 3 < 1321 1000 , α 1
α 1 -1 α 1 + α 2 -1 α 2 + • • • + α k -1 α k = k -1 + 1 α k+1 -1 .
Proof. It is a direct consequence of Lemma 6.2.

Note that the statement of Remark 6.9 actually corrects a typo in the original paper.

Theorem 6.10.

If α k ≤ n < α k+1 , C(n, k) = C(n) < (10 n) k-1 2 w n+1 . Proof. From Lemma 6.7, recall that we have C(n, k) < n n ( 10 n α 1 ) α 1 -1 α 1 ( 10 n α 2 ) α 2 -1 α 2 . . . ( 10 n α k ) α k -1 α k n α 1 n α 1 n α 2 n α 2 . . . n α k n α k = n n (10 n) k i=1 α i -1 α i k i=1 α 1 α i i n n n k i=1 1 α i k i=1 α α i -1 α i i .
It can be seen using Lemma 6.2 that:

n n 1-k i=1 1 α i ≤ n. Thus C(n, k) < n (10 n) k-1+ 1 α k+1 -1 w n k k i=1 α α i -1 α i i (by Remark 6.9) ≤ n (10 n) k-1+ 1 α k+1 -1 w n k i=1 α α i -1 α i i because w k ≤ w.
Since n < α k+1 = 1 + k i=1 α i , n ≤ k i=1 α i , and we have

k i=1 α α i -1 α i i = k i=1 α i w k ≥ n w k . 16:21 Thus C(n, k) < (10 n) k-1+ 1 α k+1 -1 w n w k ≤ (10 n) k-1 2 w n+1 as α k+1 ≥ 3 and w k ≤ w.
We can now prove Lemma 3.1:

Proof. We have:

n /3 n ≤ C(n, k)/3 n = (10 n) k-1 2 w 3 n+1 .
Remembering that k < log 2 log 2 n + 2 and w < 3, it is elementary to show that the quantity on the right is eventually decreasing to 0 and therefore bounded, which proves the result. We once again make use of the fact that 1 + 1 x x is bounded in the course of this elementary proof.

Conclusion

We are not aware of a comprehensive, reference, formal proof library on the topic of number theory, in any guise. The most comprehensive work in this direction is probably the Isabelle/HOL library on analytic number theory contributed by Eberl [START_REF] Eberl | Nine chapters of analytic number theory in isabelle/hol[END_REF], which covers a substantial part of an introductory textbook by Apostol [START_REF] Tom | Introduction to Analytic Number Theory[END_REF]. This library is based on an extensive corpus in complex analysis initially formalized by Harrison in the HOL-Light prover, and later ported to the Isabelle/HOL prover by Paulson and Li. Formal proofs also exists of a few emblematic results. The elementary fact that √ 2 is irrational was used as an example problem in a comparative study of the styles of various theorem provers [START_REF] Wiedijk | The Seventeen Provers of the World: Foreword by[END_REF], including Coq. The Prime Number theorem was proved formally for the first time by Avigad et al. [START_REF] Avigad | A formally verified proof of the prime number theorem[END_REF], using the Isabelle/HOL prover and later by Harrison [Har09] with the HOL-Light prover. Shortly after the submission of the first version of the present paper, Eberl verified [Ebe19a] Beuker's proof of Apéry's theorem [START_REF] Beukers | A note on the irrationality of ζ(2) and ζ(3)[END_REF], using the Isabelle/HOL prover, and relying on the Prime Number theorem to derive the asymptotic properties of n . Bingham was the first to formalize a proof that e is transcendental [START_REF] Bingham | Formalizing a proof that e is transcendental[END_REF], with the HOL-Light prover. Later, Bernard et al. formally proved the transcendence of both π and e in Coq [START_REF] Bernard | Formal proofs of transcendence for e and π as an application of multivariate and symmetric polynomials[END_REF].

Some of the ingredients needed in the present proof are however not specific to number theory. For instance, we here use a very basic, but sufficient, infrastructure to represent asymptotic behaviors. But "big Oh", also called Bachman-Landau, notations have been discussed more extensively by Avigad et al. [START_REF] Avigad | A formally verified proof of the prime number theorem[END_REF] in the context of their formal proof of the Prime Number Theorem, and by Boldo et al. [BCF + 10], for the asymptotic behavior of real-valued continuous functions. Affeldt et al. designed a sophisticated infrastructure for equational reasoning in Coq with Bachman-Landau notation [START_REF] Affeldt | Formalization techniques for asymptotic reasoning in classical analysis[END_REF], which relies on a non-constructive choice operator. Another example of such a secondary topic is the theory of multinomial coefficients, which is also relevant to combinatorics, and which is also defined by Hivert in his Coq library Coq-Combi [Hiv]. However, up to our knowledge this library does not feature a proof of the generalized Newton identity.

Harrison [START_REF] Harrison | Formal proofs of hypergeometric sums (dedicated to the memory of andrzej trybulec)[END_REF] presented a way to produce rigorous proofs from certificates produced by Wilf-Zeilberger certificates, by seeing sequences as limits of complex functions. His method applies to the sequence a, and can in principle prove that it satisfies the recurrence equation (3.2). However, this method does not allow for a proof that b satisfies the recurrence relation (3.2), because the summand is itself a sum but not a hypergeometric one. Up to our knowledge, there is no known way today to justify the output of the efficient algorithms of creative telescoping used here without handling a trace of provisos.

The idea to use computer algebra software (CAS) as an oracle outputting a certificate to be checked by a theorem prover, dubbed a skeptic's approach, was first introduced by Harrison and Théry [START_REF] Harrison | A skeptic's approach to combining HOL and Maple[END_REF]. It is based on the observation that CAS are very efficient albeit not always correct, while theorem provers are sound but slow. This technique thus takes the best of both worlds to produce reliable proofs requiring large scale computations. In the case of Coq, this viewpoint is especially fruitful since the kernel of the proof assistant includes efficient evaluation mechanisms for the functional programs written inside the logic [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF]. Notable successes based on this idea include the use of Pocklington certificates to check primality inside Coq [START_REF] Grégoire | A Computational Approach to Pocklington Certificates in Type Theory[END_REF] or external computations of commutative Gröbner bases, with applications for instance in geometry [START_REF] Pottier | Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics[END_REF]. Delahaye and Mayero proposed [START_REF] Delahaye | Dealing with algebraic expressions over a field in Coq using Maple[END_REF] to use CAS to help experimenting with algebraic expressions inside a proof assistant, before deciding what to prove and how to prove it. Unfortunately, their tool was not usable in our case, where algebraic expressions are made with operations that come from a hierarchy of structures.

Organizing the cooperation of a CAS and a proof assistant sheds light on their respective differences and drawbacks. The initial motivation of this work was to study the algorithms used for the automatic discovery and proof of recurrences. Our hope was to be able to craft an automated tool providing formal proofs of recurrences, by using the output of these algorithms, in a skeptical way. This plan did not work and Section 4 illustrates the impact of confusing the rational fractions manipulated by symbolic computations with their evaluations, which should be guarded by conditions on the denominators. On the other hand, proof assistants are not yet equipped to manipulate the large expressions imported during the cooperation, even those which are of a small to moderate size for the standards of computer algebra systems. For instance, we have highlighted in our previous report [START_REF] Chyzak | A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)[END_REF] the necessity to combine two distinct natures of data-structures in our libraries: one devoted to formal proofs, which may use computation inside the logic to ease bureaucratic steps, and one devoted to larger scale computations, which provides a fine-grained control on the complexity of operations. The later was crucial for the computations involved in the normalization of ring expressions during the a posteriori verification of computer-algebra produced recurrences. But it was also instrumental in our proof of Lemma 5.6.

Incidentally, our initial formal proof of Lemma 6.8 also involved this nature of calculations, with rather larger numbers1 . Indeed, the proof requires bounding the five first values of sequence α 1/an n and the straightforward strategy involves intermediate computations with integers with about 4160 decimal digits. Following a suggestion by one of the anonymous referees, we now use a less naive formula to bound α 5 . This dramatically reduces the size of the numbers involved, to the price of some additional manual bureaucracy in the proof script, mostly for evaluating binomial coefficients without an appropriate support at the level of libraries.

The Coq proof assistant is not equipped with a code generation feature akin to what is offered, for instance, in the Isabelle/HOL prover [START_REF] Hupel | A verified compiler from isabelle/hol to cakeml[END_REF]. In principle, it is possible to plug in Isabelle/HOL formal developments the result of computations executed by external, generated programs that are verified down to machine code. In the present formal proofs, Vol. 17 computation are instead carried inside the logic, using the Calculus of Inductive constructions as a programming language. Such an approach is possible in Coq because its proof-checker includes an efficient mechanism for evaluating these functional programs [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF]. Automating the correctness proofs of the program transformations required for the sake of efficiency is on-going research. In the present work, we have used the CoqEAL library [START_REF] Cohen | Refinements for Free! In Certified Programs and Proofs[END_REF], which is itself based on a plugin for parametricity proofs [START_REF] Keller | Parametricity in an impredicative sort[END_REF]. The variant proposed by Tabareau et al. [START_REF] Tabareau | Equivalences for free: univalent parametricity for effective transport[END_REF] might eventually help improving the extensibility of the refinement framework, which is a key issue. The interfaces of proof assistants are also notoriously less advanced than those of modern computer algebra. For instance, reasoning by transitivity on long chains of equalities/inequalities is often cumbersome in Coq, because of the limited support for selecting terms in an expression and for reasoning by transitivity. The Lean theorem prover [dMKA + 15] features a calc environment for proofs on transitive relations which might be used as a first step in this direction.

On several occasions in this work, we wrote more elementary versions of the proofs than what we had found in the texts we were formalizing. We partly agree with Avigad et al. [START_REF] Avigad | A formally verified proof of the prime number theorem[END_REF] when they write that this can be both frustrating and enjoyable: on one hand, it can illustrate the lack of mathematical libraries for theorems which mathematicians would find simple, such as elementary analysis for studying the asymptotics of sequences as in Section 5. Ten years later, "the need for elementary workarounds" is still present, despite his fear that it would "gradually fade, and with it, alas, one good reason for investing time in such exercises" [START_REF] Avigad | A formally verified proof of the prime number theorem[END_REF]. On the other hand, this need gives an opportunity to better understand the minimal scope of mathematical theories used in a proof, with the help of a computer. For instance, it was not clear to us at first that we could manage to completely avoid the need to define transcendental functions, or to avoid defining the constant e, base of the natural logarithm, to formalize Hanson's paper [START_REF] Hanson | On the product of the primes[END_REF]. This minimality however comes at the price of arguably more pedestrian calculations.

  Definition asympt1 R (P : R → nat → Prop) := {m : R → nat | ∀ (eps : R) (i : nat), 0 < eps → m eps ≤ i → P eps i}.

Proof.

  Since ζ(3) is Cauchy equivalent to ( bn an ) n∈N , it is sufficient to show that for any k < l, we have 0 < b l a l -b k a k . Thus it is sufficient to observe that for any k, we have 0 < b k+1 a k+1 -b k a k , which follows from Lemma 5.3. Corollary 5.5. ζ(3) -bn an = O(

  the bound above with k = 4 we get w < w 4 • α

: 1 A

 1 FORMAL PROOF OF THE IRRATIONALITY OF ζ(3) 16:23

J. Avigad and his co-authors provided the first machine-checked proof of the Prime Number theorem[START_REF] Avigad | A formally verified proof of the prime number theorem[END_REF], which was considered at the time as a formalization tour de force. Their formalization is based on a proof attributed to A. Selberg and P. Erdös.

For the current standards of proof assistants.

Acknowledgment

We wish to thank the anonymous reviewers, Alin Bostan, Frédéric Chyzak, Georges Gonthier, Marc Mezzarobba, and Bruno Salvy for their comments and suggestions. We also thank Cyril Cohen, Pierre Roux and Enrico Tassi for their help, in particular with the libraries this work depends on.

This work was supported in part by the project FastRelax ANR-14-CE25-0018-01.

16:14

A. Mahboubi

and T. Sibut-Pinote

Vol. 17:1

Proof. Easy from the definition of z, a and b.

Corollary 5.2. The sequence ( bn an ) n∈N is a Cauchy sequence, which is Cauchy equivalent to (z n ) n∈N .

The formal statement corresponding to Lemma 5.1 is:


Nima Shokri

Dany Or

Noam Weisbrod

Marc Prat

Drying of Porous Media

Open Archive TOULOUSE Archive Ouverte (OATAO)

OATAO is an open access repository that collects the work of Toulouse researchers and makes it freely available over the web where possible. This is an author-deposited version published in : http://oatao.univ-toulouse.fr/ Eprints ID : 17324

To link to this article : DOI:10.1007/s11242-015-0577-7 URL :http://dx.doi.org/10.1007/s11242-015-0577-7

To cite this version : Shokri, Nima and Or, Dany and Weisbrod, Noam and Prat, Marc Drying of Porous Media. (2015) Transport in Porous Media, Any correspondence concerning this service should be sent to the repository administrator: staff-oatao@listes-diff.inp-toulouse.fr

Drying of Porous Media

Nima Shokri 1 • Dani Or 2 • Noam Weisbrod 3 • Marc Prat 4
Drying of porous media is part of our daily experience, yet this common process is central to many environmental and engineering applications ranging from soil evaporation affecting hydrological water balance and climatic processes, to the drying of food and building materials, and driving plant life through transpiration. Drying rates from porous media may exhibit complex dynamics reflecting internal transport mechanisms and motion of phase change fronts that determine rates of drying and critically affect surface energy partitioning. These interactions and resulting drying dynamics present a challenge to the prediction of drying rates and interplay among mass and energy exchange even for fixed boundary conditions. This special issue is an outcome of a symposium that was organized in the 6th International Conference of the Interpore Society held in Milwaukee, Wisconsin, USA, in 2014, that brought together researchers from various disciplines interested in drying of porous media. The contributions included in this special issue span a wide range of topics and mechanistic aspects of porous media drying and reinforcing the importance and similarity of mechanisms and parameters influencing drying processes at different settings, considering different spatial scales and representing a blend of experimental, mechanistic theoretical and numerical approaches. Although it should be clear that all aspects of drying could not be addressed, the contributions in this special issue will give the reader a wide overview of the field and will introduce several important open problems that are the subject of active research. These include the impact of second capillary effects (liquid films, liquid bridges) on drying, the coupling between internal and external transfers, the interplay between evaporation, ion transport and precipitation-dissolution process, and the coupling between drying and poro-mechanical effects. In the following, we briefly describe the scope of each contribution. [START_REF] Yiotis | Pore network modeling of drying processes in macroporous materials: effects of gravity, mass boundary layer and pore microstructure[END_REF] presented a pore network model to describe the evaporation process from macroporous media considering various pore-scale mechanisms influencing the global drying behavior of a porous medium. Their model accounts for heterogeneity of the pore size distribution, effects of viscous flow through liquid films, and gravity and mass transfer both within the porous medium and through a boundary layer formed above the surface of the medium. [START_REF] Vorhauer | Drying with formation of capillary rings in a model porous medium[END_REF] used experiments and pore network simulations to investigate the drying of a 2D micromodel with noncylindrical throats. Their work illustrated the importance of the presence of discrete capillary liquid rings formed during the process on the observed drying behavior. They concluded that a pore network model with inclusion of capillary ring formation is a step toward the modeling of secondary capillary effects in drying of porous media in more complex geometries such as a random packing of particles. [START_REF] Haghighi | Evaporation from wavy porous surfaces into turbulent airflows[END_REF] investigated theoretically and experimentally the interactions between wavy drying surfaces and turbulent airflow above the surface to predict evaporation rates in the presence of surface roughness. Evaporation rates from wavy surfaces could be enhanced or suppressed relative to values from smooth surfaces, depending on characteristics of surface roughness (waviness) and turbulence. [START_REF] Jambhekar | Free-flow-porous-media coupling for evaporationdriven transport and precipitation of salt[END_REF] investigated the evaporation process from saline porous media and presented a numerical model to describe the coupling between the free-flow region above the surface and the transport properties of porous media influencing the drying behavior. Norouzi Rad et al. ( 2015) used X-ray tomography to quantify the effect of grain and pore size on salt precipitation during evaporation from porous media and its consequences on the dynamics and patterns of salt precipitation in saline porous media. [START_REF] Nachshon | Beyond the salt crust: on combined evaporation and subflorescent salt precipitation in porous media[END_REF] addressed the topic of subflorescent salt precipitation during evaporative drying and subsequent feedback on the evaporation process from saline porous media. The various impacts of efflorescent and subflorescent on evaporation rates and on modification of hydraulic characteristics of the porous medium due to salt precipitation are quantified. [START_REF] Scherer | Drying, shrinkage, and cracking of cementitious materials[END_REF] provides in-depth analyses of concrete drying including effects of shrinkage on compromising the resulting strength. The analysis provides new insights into the origins of the drying stress developed during drying of concrete with the associated crack formation. [START_REF] Shokri | Patterns of desiccation cracks in saline bentonite layers[END_REF] studied formation of desiccation cracks in saline clay layers with focus on the resulting cracking patterns and dynamics as influenced by salt concentration.

The special issue provides a snapshot of the range of issues and contemporary understanding of drying porous media, and issues shared among different scientific and engineering fields. We wish to thank the many dedicated reviewers for their professional and constructive efforts to improving the quality of the contributions. We are also grateful for professional and timely assistance of the Editorial office of Transport in Porous Media, and we thank the contributing authors to this special issue.

B

  Nima Shokri nima.shokri@manchester.ac.uk 1 School of Chemical Engineering and Analytical Science, The University of Manchester, Manchester, UK 2 Department of Environmental Systems Science, ETH Zürich, Zürich, Switzerland 3 Zuckerberg Institute for Water Research, Blaustein Institutes for Desert Research, Ben-Gurion University of the Negev, Midreshet Ben-Gurion, Israel

Institut de Mécanique des Fluides de Toulouse, Allée du Professeur Camille Soula, Toulouse, France


James Hartley
email: j.hartley@keele.ac.uk

Guillaume Cabanac
email: guillaume.cabanac@univ-tlse3.fr

An academic odyssey: Writing over time

Keywords: Productivity, Ageing, Longitudinal study, Writing style

In this paper we present and discuss the results of six enquiries into the first author's academic writing over the last 50 years. Our aim is to assess whether or not his academic writing style has changed with age, experience, and cognitive decline. The results of these studies suggest that the readability of textbook chapters written by Hartley has remained fairly stable for over 50 years, with the later chapters becoming easier to read. The format of the titles used for chapters and papers has also remained much the same, with an increase in the use of titles written in the form of questions. It also appears that the format of the chosen titles had no effect on citation rates, but that papers that obtained the highest citation rates were written with colleagues rather by Hartley alone. Finally it is observed that Hartley's publication rate has remained much the same for over fifty years but that this has been achieved at the expense of other academic activities.

Introduction

There have been several studies of writing in old age -both that of academics and that of other types of writers. Most academic studies are cross-sectional, that is they compare bodies of writers at different ages (e.g., see [START_REF] Pennebaker | Words of wisdom: Language use over the life span[END_REF]. Others focus on writing at a particular age (e.g., [START_REF] Skinner | Intellectual self-management in old age[END_REF][START_REF] Sommer | My last journal article[END_REF]. Others are longitudinal (e.g., [START_REF] Hartley | Writing through time: Longitudinal studies of the effects of new technology on writing[END_REF][START_REF] Todorovsky | On the working time budget of the university teacher[END_REF][START_REF] Todorovsky | Follow-up study: On the working time budget of a university teacher. 45 years self-observation[END_REF] -but these are much rarer. Cross-sectional studies require the readers to assume that the different age-groups are similar in every respect -except age -but this of course is unlikely. Age-specific studies are biographical and provide case-histories at a particular point in time. Longitudinal studies compare the same writers at different ages, but here the readers have to assume that the only thing that changes in their samples is their age. Few longitudinal studies mention other changes in, for example, life-styles, or even the tools that writers use to write over timefrom pen/pencil to typewriter, word-processor and, for example, voice-activated computers (but see [START_REF] Hartley | Speaking versus typing: A case-study of the effects of using voice-recognition software on academic correspondence[END_REF].

These studies differ in other respects too. Some researchers focus on using statistical packages to analyse the use of various grammatical features over time, as well as particular kinds of words (e.g. emotional, cognitive, personal: e.g., see [START_REF] Graesser | Coh-Metrix: Providing multilevel analyses of text characteristics[END_REF][START_REF] Markowitz | Linguistic traces of a scientific fraud: The case of Diederik Stapel[END_REF][START_REF] Pennebaker | How authors' forgettable words reveal their personality and social behaviors[END_REF] whereas others, using simpler methods, look at topics such as word and sentence lengths, and readability (e.g., [START_REF] Hartley | Writing through time: Longitudinal studies of the effects of new technology on writing[END_REF]. Other authors have used such tools in forensic studies to see if the authorship of a document is consistent, and whether or not different texts (or parts of texts) attributed to one author were actually written by someone else (see, e.g., Boyd & Pennebaker, in press;[START_REF] Labbé | Experiments on authorship attribution by intertextual distance in English[END_REF][START_REF] Savoy | Authorship attribution: A comparative study of three text corpora and three languages[END_REF].

In this paper we seek to assess whether a single academic author's writing style has remained much the same or changed over a period of fifty years (see "Lifetime Achievement Award: James Hartley", 2014). Why, might we ask, should the writing styles of academics change over time? Well, improvements with practice over time may make writers more efficient, and learning from experience might lead to more effective writing. Writers might benefit from observing excellent practice elsewhere -and trying to copy it. Different formats for titles, abstracts, introductions and discussions may be tried and tested, leading to a change or bias in one way of writing or another.

In this paper we report six studies which raise questions such as these about writing over time by the first author of this paper:

• In Study 1 [START_REF] Hartley | Writing through time: Longitudinal studies of the effects of new technology on writing[END_REF] were interested in the readability of texts produced by three different authors over the time-period 1972-2000. They showed that each author differed from each other, but that there were few changes in their individual writing styles over time -as measured by [START_REF] Flesch | A new readability yardstick[END_REF] readability scores. Table 1 shows some of the data provided by Hartley et al.

• In Study 2 we replicated these studies by examining the readability of book chapters written by the first author over the last ten years. Our aim was to see if the data reflected any progress in his desire to make his book chapters easier to read. Table 2 shows some success in this respect.

• In Study 3 we examined the styles of titles written by the first author and listed in his current short curriculum vitae. 1 Here we looked to see if there were different patterns in the use of question marks and colons for book chapter titles, and the titles of academic articles over a period of fifty years. We found an increase in the use of titles with question marks in the last 25 years. A larger use of question marks is also apparent in the author's recent blogs.

• In Study 4 we examined whether or not the first author's articles that contained colons and question marks in their titles were cited more or less often than were those titles that were written in grammatically simpler text. Here we found an increase in the numbers of question marks and colons in the titles of more recent papers, but that this was not reflected in citation rates.

• In Study 5 we looked to see if articles written with colleagues were cited more than articles written by Hartley alone. Here there was a significant difference in this respect for the most highly cited 20 papers, but no significant differences between them when a larger sample was used.

• In Study 6 we examined Hartley's output to see if it was maintained over the years or whether or not there were changes in this respect. We found that there were no changes in the rate of output over time, but this was achieved by reducing other activities.

Study 1. Writing over time

In this study Hartley, Howe, and McKeachie first illustrated how the methods they used to write had changed dramatically over a thirty-year time period [START_REF] Hartley | Writing through time: Longitudinal studies of the effects of new technology on writing[END_REF]. In Hartley's case, he progressed from writing drafts in longhand, to having different versions first typed by secretaries and then word-processed by them until he finally word-processed them himself. Currently he writes, edits, and revises each of numerous drafts simultaneously, using word-processing software. His colleagues, Howe and McKeachie, similarly changed their ways of writing over time, and indeed McKeachie dictated some of his speeches for a part of this period.

Table 1 shows an extract from the data obtained. These data showed the results obtained in term of readability scores for seven book chapters written by Hartley over a period of approximately 30 years. It can be seen that the scores vary very little, despite the considerable changes in the ways that they were written. a Flesch scores range from 0 to 100. The higher the score the more readable the text (see [START_REF] Flesch | A new readability yardstick[END_REF]. Scores below 30 are deemed 'very difficult to read' and are typical in academic text. Similar data are presented for two other colleagues in [START_REF] Hartley | Writing through time: Longitudinal studies of the effects of new technology on writing[END_REF].

Study 2. Revisiting Study 1

In Study 2 we wished to bring the findings of Study 1 up to date. Not only had Hartley continued to write book chapters but he had become more aware from the earlier results of the need to make them easier to read.

In this study we report the results for six book chapters published between 2002 and 2015, using the same format as that used in Table 1. The readability measures shown in Table 2 indicate that, on the whole, these later chapters are easier to read than the earlier ones. Indeed, the median Flesch score for early chapters is 44.0 compared to 50.5 for the later chapters. Study 3. Did the forms of title chosen for publications differ over time?

Titles come in many different forms (see [START_REF] Hartley | Academic writing and publishing: A practical handbook[END_REF], for 13 types). The three most common are:

• a simple sentence (Titles come in many different forms)

• titles with colons (Titles with colons: three different ways), and

• titles with question marks (How many types of titles are there?).

In Study 3 we were interested to see if there had been any changes in the types of titles that Hartley had used over time. To answer this question we examined the titles of publications listed in Hartley's short curriculum vitae from 1964. First of all we counted the number of colons and the number of question marks used in book chapters and articles (Table 3). These data show that there were no differences in the use of titles with colons or question marks for book chapters, but that colons were used more than question marks in the titles of articles. Yet, there was no significant association between the type of publication and the form of title, χ 2 (1, N = 60) = 1.50, p = 0.22. The above results were obtained using data from the first author's short curriculum vitae. The next question we asked was 'Were there any differences over time?' Here we re-analysed these data in terms of a 50:50 split -in order to compare titles written during with those written during 1991-2014 (see Table 4). There was a significant relation between the time periods and the use of colons and question marks in titles, χ 2 (1, N = 60) = 4.54, p = 0.03. The results suggest that Hartley changed over time to using more titles with question marks in his publications.

Finally, we looked at the format of the titles used by Hartley in his recent interest in writing academic blogs. Here he published 11 blogs between 2012 and 2015. Five of these had titles with question marks, 1 used two question marks, 1 used a question mark and a colon, 2 used colons, and 2 were simple sentences. So simplifying, there were 7 titles with question marks, 3 with a colon, and 2 simple sentences. It appears then that Hartley used more titles written with question marks in his blogs than he did in his more standard publications. However, titles with question marks are more common in this genre. Study 4. Did the format of a title influence an article's citation rate?

Next, we looked to see if the format of the title of an article influenced its citation rate. Here we examined the titles of articles and their citation rates provided by Google Scholar for the first author.2 Being aware of the issues raised about this inappropriate data source [START_REF] Jacsó | Metadata mega mess in Google Scholar[END_REF], we manually checked each record and discarded inappropriate ones. We recorded the format of the title for the top 100 cited publications. In this sample of 100 titles, the most cited title had been cited 267 times and the lowest 8. We then looked at the format of these titles in terms of question marks, colons, and simple sentences. Table 5 shows the results. These data show that only 15% of the titles were written in the form of questions, and that titles with colons or simple sentence titles were roughly equal in terms of their number (about 43%). Furthermore, for all three types of title, there were large ranges in terms of their citations rates, with the exception of titles with question marks. The data are so widely spread that it is safe to report that there were no statistically significant differences between the citation rates of Hartley's papers using these three types of title. This conclusion replicates that found in earlier studies (see [START_REF] Hartley | Planning that title: Practices and preferences for titles with colons in academic articles[END_REF]. Other studies of colonic usage, using larger databases have, however, found more varied results. The use of colons in titles seems to be more discipline based than was thought to be the case -there being more colonic titles in the medical sciences than in engineering and technology [START_REF] Hartley | Titles are the hardest thing: How can we make them more effective[END_REF][START_REF] Lewison | What's in a title? Numbers of words and the presence of colons[END_REF]. [START_REF] Buter | Non-alphanumeric characters in titles of scientific publications: An analysis of their occurrence and correlation with citation impact[END_REF] for instance, also reported that hyphens and colons were common in some disciplines and that including them correlated positively with impactand they advised authors to stick to their disciplinary practices.

Study 5. Are articles written with colleagues cited more than single-authored ones?

There is some debate in the literature over whether or not articles written with colleagues get cited more than articles written alone [START_REF] Abrizah | Sixty-four years of informetrics research: Productivity, impact and collaboration[END_REF][START_REF] Didegah | Which factors help authors produce the highest impact research? Collaboration, journal and document properties[END_REF][START_REF] Gazni | The long-term influence of collaboration on citation patterns[END_REF]. In this study it was possible to examine this question using data from Google Scholar again to compare the citation rates for articles written by Hartley and colleagues with those written by Hartley alone.

One problem with citation data, of course, is that they are influenced by the date of publication: citation rates are usually higher, the older the article. In this study we examined the citation rates for the most highly cited 100 articles in Google Scholar according to whether or not they were written by a single author (Hartley) or with other(s). Table 6 shows the data we obtained. These results offer no support for the notion that jointly-authored papers are cited more frequently that single authored ones. However, further inspection of the raw data suggested that there was a difference between the citation rates for single and multi-authored papers when the most-highly cited papers were compared. Table 7 shows the results obtained for the top ten papers in each group. These latter data do show some support for the notion that papers with multiple authors are cited more than singly-authored papers, U = 15.5, p = 0.001 (the titles of these papers and their citation rates are presented in the Appendix).

The data thus confirm the earlier findings showing that multi-author papers may be cited more than single-authored ones. But, we note in passing, that exactly what is meant by collaboration, and how it is measured, are actually complex matters [START_REF] Laudel | What do we measure by co-authorships[END_REF]. It is not clear to us, for example, just how the single-authored papers differ in content from the multiple-authored ones. It is also possible that the journals in which these papers are published may be an important factor.

Study 6. Declining over time

Finally, it is to be expected that publication rates will decline over time as writers get older. Other things have to be taken into account. Consider the following two quotations from a study on academic writing in old age [START_REF] Hartley | To cite or not to cite: Author self-citations and the impact factor[END_REF]: "I've been lucky to have kept reasonably fit. But my energy now (as I approach 90) is fading. In the first 20 years of retirement I published 20 journal papers, 4 books and 11 book chapters. Now I am content to have just one job a year." "I am better able to devote large blocks of time to writing. But probably, also a little slower, physically, and possibly, mentally." Table 8 presents some data in this respect by examining the numbers of Hartley's publications over five ten-year periods.

Table 8 The number of publication in 10 year periods (data from short curriculum vitae) 1965-1974 1975-1984 1985-1994 1995-2004 These data suggest that numbers of books and chapters produced over time are perhaps slowing down, but that the publication rates for articles have been maintained. What the studies in this table do not show is that Hartley's productivity has been maintained whilst other activities have been abandoned (e.g., teaching, administration, examining, presenting at and attending conferences, supervising dissertations, etc.). Thus whilst one activity (writing) has been sustained, others have been reduced or abandoned altogether. Basically these ideas support the views of [START_REF] Hess | Selective engagement of cognitive resources: Motivational influences on older adults' cognitive functioning[END_REF], who argues that, relative to younger adults, older ones become more sensitive to the contexts of performance and more selective in their allocation of cognitive resources. As Hess puts it: "For the most part, selective engagement may be viewed as an adaptive process, as older adults adjust their levels of participation to be in line with the costs of such engagement and to conserve resources to maximize performance in the most personally relevant situations." (Hess, 2014, p. 401) Hartley has conserved his enthusiasm for academic writing whilst at the same time reducing his interest in several other academic pursuits.

Publication

Summary

In this paper we have looked to see if there have been changes in the writing style of the first author over a period of 50 years. In brief it appears that:

1. The readability of Hartley's book chapters (as measured by the Flesch Reading Ease score) has remained remarkably similar for over fifty years, but there is a suggestion that they have got easier to read in the latter years. 2. The format of the titles used for chapters and articles initially remained much the same for the earlier period but, following his wish to make the text easier to read, the use of titles with question marks increased in the latter period. 3. The format of the titles used for books, chapters, and articles had no significant effect on their citation rates. 4. Hartley's papers with higher citations were written with colleagues and have been cited more frequently than similar papers written by Hartley alone: for less highly cited papers there appears to be no significant difference in this respect.

5. Hartley's publication rates -over 10 year periods -suggest that in the later years, the number of books and book chapters has declined but that the publication rates for articles has remained much the same. 6. This output has been maintained by cutting back on other competing activities in the last few years.

Table 1

 1 Readability statistics for book chapters written by JamesHartley from 1972Hartley from -2000

	Date	1972 1978 1982	1987	1995	1999 2000
	Number of words sampled	1,032	978	990 1,125 1,014 1,026	931
	Number of sentences	45	45	38	48	42	42	41
	Average no. words per sentence	23	22	26	23	24	24	23
	Average % passives sentences	35	13	21	14	21	19	27
	Flesch score a	42	36	39	50	47	44	53
	Grade-level	12	12	12	11	12	11	10

Table 2

 2 Readability statistics for book chapters written by JamesHartley from 2001Hartley from -2014

	Date	2001 2004a 2004b	2007	2012	2015
	Number of words sampled	1,391	1,885	920 1,825 2,034 1,707
	Number of sentences	32	86	42	79	92	68
	Average no. words per sentence	20	22	21	23	22	15
	Average % passives sentences	11	30	23	21	20	10
	Flesch score	51	50	44	44	55	51
	Grade-level	11	11	11	11	11	10

Table 3

 3 Number of titles with colons and question marks in Hartley's book chapters and articles Number of titles with. . .

	Type	colons	question marks
	Chapters	5	5
	Articles	35	15

Table 4

 4 Number of titles with colons and question marks in Hartley's book chapters and articles over time Number of titles with. . .

	Years	colons question marks
	1965-1990	17	3
	1991-2014	23	17

Table 5

 5 The medians (and ranges) of the citation rates for three different types of title (from a sample of 100 chapters and papers)

		Simple sentences Titles with colons Titles with question marks
	Median	18	21	23
	Range	8-211	8-267	8-59
	N	45	40	15

Table 6

 6 The median citation rates for 39 single-authored and 61 multi-authored articles

		Single authors Multiple authors
	Median	22	23
	Range	10-95	9-207
	N	39	61

Table 7

 7 The median citation rates for the top ten single-authored and multi-authored articles

		Single authors Multiple authors
	Median	56	130
	Range	34-95	68-207
	N	10	10

This 'short curriculum vitae' lists Hartley's major publications (for the sake of convenience). It includes, for example, only 5 of his

publications with undergraduates (seeHartley, 2014a), and short notes, letters, etc. are not included.

See http://scholar.google.com/citations?user=7Ls3LsgAAAAJ

Acknowledgements We are grateful to two anonymous referees for helpful comments and suggestions, and particularly to the one who cast our data into graphical forms.

Appendix. Citation rates for single author and multiple authors

Data from Table 9 and Table 10 were used in Study 5.