Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL

ABSTRACT

We give an overview of our formalizations in the proof assistant Isabelle/HOL of certain irrationality and transcendence criteria for infinite series from three different research papers: by Erdős and Straus, Hančl, and Hančl and Rucki. Our formalizations in Isabelle/HOL can be found on the Archive of Formal Proofs. Here we describe selected aspects of the formalization and discuss what this reveals about the use and potential of Isabelle/HOL in formalizing modern mathematical research, particularly in these parts of number theory and analysis.

KEYWORDS:

• Transcendence
• irrationality
• series
• interactive theorem proving
• Isabelle/HOL
• proof assistants

Correction Statement

This article has been republished with minor changes. These changes do not impact the academic content of the article.

Acknowledgements

The authors thank the ERC for their support through the ERC Advanced Grant ALEXANDRIA (Project GA 742178). We thank the anonymous reviewers for their useful suggestions that improved our exposition. We also thank Jaroslav Hančl and Pavel Rucki for a helpful email suggesting a fix for the slight mistake in their proof [24, Theorem 2.1], Iosif Pinelis for his useful explanation on MathOverflow regarding an argument in the proof of Theorem 2.2 in the same article⁸ and Anthony Bordg for a discussion on the necessity of formalizing advanced mathematics even if the proofs of the prerequisites are not formalized.

7 Declaration of Interest

No potential conflict of interest was reported by the author(s).

Notes

1 isabelle.in.tum.de/dist/library/HOL

2 www.isa-afp.org

3 The proof of Roth’s theorem itself has not been formalized; see Section 5.

4 https://isabelle.in.tum.de/

5 These can also be found under “Documentation” on the Isabelle webpage.

6 as x approaches the filter F

7 Here, $o(·)$ is the ‘little o’ notation, and ${\phi }_{n+1}(x)\in o({\phi }_n(x))$ as $x\to L$ is equivalent to $\underset{x\to L}{\lim }{\phi }_{n+1}(x)/{\phi }_n(x)=0$.

8 The reader may notice that this development too seems to depend on the AFP entry for the Prime Number Theorem [10]. However we only use some technical lemmas from that development. Primes play no role here.

9 https://mathoverflow.net/questions/323069/why-is-this-series-summable