[isabelle] New in the AFP: The Transcendence of Certain Infinite Series

The Transcendence of Certain Infinite Series
  by Angeliki Koutsoukou-Argyraki and Wenda Li

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.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.