swMATH ID: 38035
Software Authors: Angeliki Koutsoukou-Argyraki; Wenda Li
Description: Irrationality_J_Hancl: Irrational Rapidly Convergent Series. We formalize with Isabelle/HOL a proof of a theorem by J. Hancl asserting the irrationality of the sum of a series consisting of rational numbers, built up by sequences that fulfill certain properties. Even though the criterion is a number theoretic result, the proof makes use only of analytical arguments. We also formalize a corollary of the theorem for a specific series fulfilling the assumptions of the theorem.
Homepage: https://www.isa-afp.org/entries/Irrationality_J_Hancl.html
Dependencies: Isabelle
Related Software: Pratt_Certificate; Quaternions; Irrational_Series_Erdos_Straus; Transcendence_Series_Hancl_Rucki; Amicable Numbers; Octonions; Aristotles_Assertoric_Syllogistic; Archive Formal Proofs; MathOverflow; kepler98; HOL; Isabelle/HOL; Isabelle
Referenced in: 1 Publication

Referenced by 1 Author

1 Koutsoukou-Argyraki, Angeliki

Referencing Publications by Year