Formal Proof of Transcendence of the Number e. Part II

Yasushige Watase

doi:10.2478/forma-2024-0009

Abstract

In this article we formalize the main part of Hurwitz’s proof of the transcendence of the number e in the Mizar language. The previous article prepared the necessary definitions and lemmas. Here we deal with main crucial steps of the proof.

References

Alan Baker. Transcendental Number Theory. Cambridge University Press, 1990.
Search in Google Scholar Back to article
Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.
Open DOI Search in Google Scholar Back to article
Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.
Open DOI Search in Google Scholar Back to article
Sophie Bernard, Yves Bertot, Laurence Rideau, and Pierre-Yves Strub. Formal proofs of transcendence for e and π as an application of multivariate and symmetric polynomials. In Jeremy Avigad and Adam Chlipala, editors, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 76–87. ACM, 2016. doi:10.1145/2854065.2854072.
Open DOI Search in Google Scholar Back to article
Jesse Bingham. Formalizing a proof that e is transcendental. Journal of Formalized Reasoning, 4:71–84, 2011.
Search in Google Scholar Back to article
Manuel Eberl. The transcendence of e. Archive of Formal Proofs, 2017. https://isa-afp.org/entries/E_Transcendental.html, Formal proof development.
Search in Google Scholar Back to article
Matsusaburo Fujiwara. Algebra vol 2, Japanese. Uchida Rokakuho Publishing Co., Ltd, 1st edition, 1929.
Search in Google Scholar Back to article
Adolf Hurwitz. Beweis der Transcendenz der Zahl e. Mathematische Annalen, 43:220–221, 1893.
Search in Google Scholar Back to article
Artur Korniłowicz. Elementary number theory problems. Part VIII. Formalized Mathematics, 31(1):87–100, 2023. doi:10.2478/forma-2023-0009.
Open DOI Search in Google Scholar Back to article
Artur Korniłowicz and Christoph Schwarzweller. The first isomorphism theorem and other properties of rings. Formalized Mathematics, 22(4):291–301, 2014. doi:10.2478/forma-2014-0029.
Open DOI Search in Google Scholar Back to article
Artur Korniłowicz, Adam Naumowicz, and Adam Grabowski. All Liouville numbers are transcendental. Formalized Mathematics, 25(1):49–54, 2017. doi:10.1515/forma-2017-0004.
Open DOI Search in Google Scholar Back to article
Serge Lang. Introduction to Transcendental Numbers. Addison-Wesley Pub. Co., 1966.
Search in Google Scholar Back to article
Norman D. Megill and David A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019.
Search in Google Scholar Back to article
Robert Milewski. Fundamental theorem of algebra. Formalized Mathematics, 9(3):461–470, 2001.
Search in Google Scholar Back to article
Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, pages 625–635, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-79876-5 37.
Open DOI Search in Google Scholar Back to article
Karol P¡k. Eigenvalues of a linear transformation. Formalized Mathematics, 16(4):289–295, 2008. doi:10.2478/v10037-008-0035-x.
Open DOI Search in Google Scholar Back to article
Christoph Schwarzweller. On roots of polynomials over F [X]/[angbracketleft]p[angbracketright]. Formalized Mathematics, 27(2):93–100, 2019. doi:10.2478/forma-2019-0010.
Open DOI Search in Google Scholar Back to article
Christoph Schwarzweller. Normal extensions. Formalized Mathematics, 31(1):121–130, 2023. doi:10.2478/forma-2023-0011.
Open DOI Search in Google Scholar Back to article
Yasushige Watase. Formal proof of transcendence of the number e. Part I. Formalized Mathematics, 32(1):111–120, 2024. doi:10.2478/forma-2024-0008.
Open DOI Search in Google Scholar Back to article
Yasushige Watase. Derivation of commutative rings and the Leibniz formula for power of derivation. Formalized Mathematics, 29(1):1–8, 2021. doi:10.2478/forma-2021-0001.
Open DOI Search in Google Scholar Back to article
Freek Wiedijk. Formalizing 100 theorems. Available online at http://www.cs.ru.nl/~freek/100/.
Search in Google Scholar Back to article

Formal Proof of Transcendence of the Number e. Part II

Abstract

Paradigm

My account