Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:7NEYN3VRrecord.jsonopen to challenge →
read the original 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\H{o}s and Straus (1974), Han\v{c}l (2002), and Han\v{c}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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.