Irrationality and transcendence criteria for infinite series in Isabelle/HOL

DOI10.1080/10586458.2021.1980465MaRDI QIDQ5094474zbMATH OpenOpenAlexFDO

Authors Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson

Publication date 3 August 2022

Published in Experimental Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://arxiv.org/abs/2101.05257

zbMATH Keywords

interactive theorem provingIsabelle/HOLproof assistants

Mathematics Subject Classification ID

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)

Recommendations

• A formal proof of the irrationality of \(\zeta(3)\)
• scientific article; zbMATH DE number 7106480
• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• scientific article; zbMATH DE number 1670741
• Formal power series

Cites work

• scientific article; zbMATH DE number 3865392 (Why is no real title available?)
• scientific article; zbMATH DE number 3578925 (Why is no real title available?)
• scientific article; zbMATH DE number 3624817 (Why is no real title available?)
• scientific article; zbMATH DE number 1154148 (Why is no real title available?)
• scientific article; zbMATH DE number 3338601 (Why is no real title available?)
• scientific article; zbMATH DE number 2216753 (Why is no real title available?)
• A corrected quantitative version of the Morse lemma
• A formal proof of the Kepler conjecture
• A proof of the Kepler conjecture
• A theorem on transcendence of infinite series
• A theorem on transcendence of infinite series. II
• Complex Analysis
• Criterion for irrational sequences
• Formal proof - the four color theorem
• Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
• Hammering towards QED
• Irrational rapidly convergent series
• Isabelle/HOL. A proof assistant for higher-order logic
• Mahler functions and transcendence
• On certain series with irrational values.
• On the irrationality of certain series
• Rational approximations to algebraic numbers
• Some number theoretic results
• The foundation of a generic theorem prover
• The transcendence of certain infinite series
• Type classes and filters for mathematical analysis in Isabelle/HOL
• Verified Real Asymptotics in Isabelle/HOL

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
• scientific article; zbMATH DE number 1696609 (Why is no real title available?)
• Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project

Describes a project that uses

Uses Software

• Irrational_Series_Erdos_Straus
• Transcendence_Series_Hancl_Rucki
• Irrationality_J_Hancl
• Archive Formal Proofs
• kepler98
• Automath
• Isabelle/HOL

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)