Formal Proof of Transcendence of the Number e. Part I

Yasushige Watase

doi:10.2478/forma-2024-0008

Abstract

In this article, we prove the transcendence of the number e using the Mizar formalism, following Hurwitz’s proof. This article prepares the necessary definitions and lemmas. The main body of the proof will be presented separately.

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
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
Charles Hermite. Sur la fonction exponentielle. Gauthier-Villars, 1874.
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. Di erentiability of polynomials over reals. Formalized Mathematics, 25(1):31–37, 2017. doi:10.1515/forma-2017-0002.
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
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. Field extensions and Kronecker’s construction. Formalized Mathematics, 27(3):229–235, 2019. doi:10.2478/forma-2019-0022.
Open DOI Search in Google Scholar Back to article
Christoph Schwarzweller and Agnieszka Rowińska-Schwarzweller. Simple extensions. Formalized Mathematics, 31(1):287–298, 2023. doi:10.2478/forma-2023-0023.
Open DOI Search in Google Scholar Back to article
Christoph Schwarzweller, Artur Korniłowicz, and Agnieszka Rowińska-Schwarzweller. Some algebraic properties of polynomial rings. Formalized Mathematics, 24(3):227–237, 2016. doi:10.1515/forma-2016-0019.
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 I

Abstract

Paradigm

My account