Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
Open Access
- 21 October 2021
- journal article
- research article
- Published by Taylor & Francis in Experimental Mathematics
- Vol. 31 (2) , 401-412
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
All Related Versions
This publication has 18 references indexed in Scilit:
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL2013
- A proof of the Kepler conjectureAnnals of Mathematics, 2005
- The Transcendence of Certain Infinite SeriesRocky Mountain Journal of Mathematics, 2005
- A Theorem on Transcendence of Infinite Series IIJournal of Number Theory, 2001
- A Theorem on Transcendence of Infinite SeriesRocky Mountain Journal of Mathematics, 2000
- Criterion for Irrational SequencesJournal of Number Theory, 1993
- The foundation of a generic theorem proverJournal of Automated Reasoning, 1989
- Inverse piezoelectric effect and electrostrictive effect in polarized poly(vinylidene fluoride) filmsJournal of Materials Science, 1975
- On the irrationality of certain seriesPacific Journal of Mathematics, 1974
- Some number theoretic resultsPacific Journal of Mathematics, 1971