Irrationality and transcendence criteria for infinite series in Isabelle/HOL
DOI10.1080/10586458.2021.1980465OpenAlexW3208345691MaRDI QIDQ5094474FDOQ5094474
Authors: Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. 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
Recommendations
Mechanization of proofs and logical operations (03B35) Transcendence (general theory) (11J81) Formalization of mathematics in connection with theorem provers (68V20) Approximation to algebraic numbers (11J68) Software, source code, etc. for problems pertaining to number theory (11-04) Digital mathematics libraries and repositories (68V35)
Cites Work
- A proof of the Kepler conjecture
- Isabelle/HOL. A proof assistant for higher-order logic
- Mahler functions and transcendence
- Type classes and filters for mathematical analysis in Isabelle/HOL
- Formal proof - the four color theorem
- Complex Analysis
- Title not available (Why is that?)
- Rational approximations to algebraic numbers
- A theorem on transcendence of infinite series. II
- Title not available (Why is that?)
- The transcendence of certain infinite series
- Title not available (Why is that?)
- On the irrationality of certain series
- On certain series with irrational values.
- The foundation of a generic theorem prover
- Criterion for irrational sequences
- Title not available (Why is that?)
- Title not available (Why is that?)
- Some number theoretic results
- Hammering towards QED
- A formal proof of the Kepler conjecture
- Title not available (Why is that?)
- A theorem on transcendence of infinite series
- Verified Real Asymptotics in Isabelle/HOL
- A corrected quantitative version of the Morse lemma
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Irrational rapidly convergent series
Cited In (7)
- Cardinals in Isabelle/HOL
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Using Isabelle/HOL to verify first-order relativity theory
- A formal proof of the irrationality of \(\zeta(3)\)
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Title not available (Why is that?)
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
Uses Software
This page was built for publication: Irrationality and transcendence criteria for infinite series in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5094474)
