The Transcendence of Certain Infinite Series

Angeliki Koutsoukou-Argyraki 🌐 and Wenda Li 🌐

March 27, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Transcendence_Series_Hancl_Rucki