Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
DOI10.1080/10586458.2021.1980465OpenAlexW3208345691MaRDI QIDQ5094474
Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence Charles Paulson
Publication date: 3 August 2022
Published in: Experimental Mathematics (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2101.05257
Mechanization of proofs and logical operations (03B35) Transcendence (general theory) (11J81) Software, source code, etc. for problems pertaining to number theory (11-04) Approximation to algebraic numbers (11J68) Formalization of mathematics in connection with theorem provers (68V20) Digital mathematics libraries and repositories (68V35)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On certain series with irrational values.
- Criterion for irrational sequences
- Isabelle/HOL. A proof assistant for higher-order logic
- A theorem on transcendence of infinite series. II
- The foundation of a generic theorem prover
- Mahler functions and transcendence
- A corrected quantitative version of the Morse lemma
- A proof of the Kepler conjecture
- Some number theoretic results
- The transcendence of certain infinite series
- Irrational rapidly convergent series
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Verified Real Asymptotics in Isabelle/HOL
- Hammering towards QED
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- Rational approximations to algebraic numbers
- Complex Analysis
- On the irrationality of certain series
- A theorem on transcendence of infinite series
This page was built for publication: Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
