Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson
TL;DR
This paper discusses the formalization of irrationality and transcendence criteria for infinite series in Isabelle/HOL, demonstrating the proof assistant's capabilities in modern number theory and analysis.
Contribution
It presents the first formalizations of these criteria in Isabelle/HOL, showcasing their application to advanced mathematical research.
Findings
Formalizations are available on the Archive of Formal Proofs.
The work highlights Isabelle/HOL's potential in formalizing complex mathematical concepts.
The formalizations facilitate rigorous verification of number theory results.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.