The Transcendence of Certain Infinite Series

Angeliki Koutsoukou-Argyraki 🌐 and Wenda Li 🌐

March 27, 2019


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