The reviewed record of science sign in
Pith

arxiv: 2101.05257 · v2 · pith:7NEYN3VR · submitted 2021-01-08 · cs.LO · math.LO

Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL

Angeliki Koutsoukou-Argyraki , Wenda Li , Lawrence C. Paulson This is my paper

Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:7NEYN3VRrecord.jsonopen to challenge →

classification cs.LO math.LO
keywords isabellecriteriaformalizationsinfiniteirrationalityresearchseriestranscendence
0
0 comments X
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.