The Transcendence of Certain Infinite Series

Angeliki Koutsoukou-Argyraki and Wenda Li

27 March 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

Depends On


Related Entries