Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Koutsoukou-Argyraki, A https://orcid.org/0000-0002-8886-5281
Paulson, LC https://orcid.org/0000-0003-0288-4279
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 (1974), Hančl (2002), and Hančl and Rucki (2005). 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.
Description
Keywords
Transcendence, irrationality, series, interactive theorem proving, Isabelle, HOL, proof assistants
Journal Title
Experimental Mathematics
Conference Name
Journal ISSN
1058-6458
1944-950X
1944-950X
Volume Title
Publisher
Informa UK Limited
Publisher DOI
Rights
All rights reserved
Sponsorship
European Research Council (742178)