## Irrationality_J_Hancl

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 |

### Referenced in 1 Serial

1 | Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) |

### Referenced in 2 Fields

1 | Mathematical logic and foundations (03-XX) |

1 | Computer science (68-XX) |