### Abstract

We formalize the proofs of two transcendence criteria by J. Hančl and P. Rucki that assert the transcendence of the sums of certain infinite series built up by sequences that fulfil certain properties. Both proofs make use of Roth's celebrated theorem on diophantine approximations to algebraic numbers from 1955 which we implement as an assumption without having formalised its proof.

### License

BSD License

### Topics

- Mathematics/Analysis
- Mathematics/Number theory

### Session Transcendence_Series_Hancl_Rucki

- Transcendence_Series

### Depends on

- The Prime Number Theorem

### Auto-related entries

- Factorization of Polynomials with Algebraic Coefficients
- The Hermite–Lindemann–Weierstraß Transcendence Theorem
- Hilbert’s Nullstellensatz
- Algebraic Numbers in Isabelle/HOL

## Cite

×

Transcendence_Series_Hancl_Rucki-AFP

    @article{Transcendence_Series_Hancl_Rucki-AFP,
      author  = {Angeliki Koutsoukou-Argyraki and Wenda Li},
      title   = {The Transcendence of Certain Infinite Series},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Transcendence_Series_Hancl_Rucki.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Mar 28, 2019 : Isabelle2018