@MISC{E_TRANS1.MIZ,
  AUTHOR = {Watase, Yasushige},
  TITLE = {Formal Proof of Transcendence of the Number $e$. {P}art {I}},
  DAY = {17},
  MONTH = {November},
  YEAR = {2024},
  ADDRESS1 = {Suginami-ku Matsunoki 6, 3-21 Tokyo\\Japan},
SUMMARY = {In this article, we prove the transcendence of the number $e$ using the Mizar formalism 
   \cite{Mizar-State-2015}, along with Hurwitz's proof \cite{HURWITZ:1893}.
  This subject has been implemented over the past decade in other theorem provers, such as 
   HOL Light \cite{Bingham:2011} and Coq   \cite{BernardBRS:2016}. 
  This article prepares the necessary definitions and lemmas. The main body of the proof will be presented separately. \\
  At the beginning, we formalize a lemma about algebraic numbers, namely for a polynomial over $\mathbb{Z}$ which has a root equal to $e$, 
  if suppose $e$ is algebraic, in another word $e$ is not transcendental number as theorem. ($\textit{ref}. \ \mathrm{E\_TRANS1:11)}$. 
  It corresponds to the equation (3) of \cite{HURWITZ:1893}. \par
  Then, we define a polynomial transformation $F$. For a polynomial $f$ over $\mathbb{Q}$ with degree $r$, 
  we introduce a functor: ($\textit{ref}. \ \mathrm{E\_TRANS1:def \ 10} $)
  $$ F: f(x) \mapsto f(x) + f^{\prime}(x) + f^{\prime \prime}(x) + \cdots + f^{(r)}(x) \ \ $$
  In Hurwitz's proof he defines $F(x) = f(x) + f^{\prime}(x) + f^{\prime \prime}(x) + \cdots + f^{(r)}(x) $ 
  as equation (1) in \cite{HURWITZ:1893}. In the actual formalization for constructing $F$ we generate a 
  finite sequence of polynomials defined by $G = \{ f^{(i)}(x)\}$, then $F$ is formalized as the summation of 
  it, namely $(F = Sum G)$. Since higher order derivations for a ring have been implemented in \cite{RINGDER1.ABS}, 
  we are able to formalize $i^{th}$ component of $G$. Then we apply the mean value theorem to 
  $e^{x}F(x)$ on an interval and formalize the following equation quoted as equation (2) 
  in \cite{HURWITZ:1893}:  ($\textit{ref}. \ \mathrm{E\_TRANS1:34} $)
  $$F(x) - e^{x}F(0) = -xe^{(1-\vartheta) x }{f(\vartheta x)}.$$ 
  The rest of the section is devoted to preparing lemmas to define the particular polynomial 
   $f(x) =  \frac{1}{(p-1)!}x^{p-1}(1-x)^{p}(2-x)^{p}\cdots (n-x)^{p}$ which play an important role of the main proof.},
  MSC2010 = {11J81,03B35},
  KEYWORDS = {Transcendental Number; Hurwitz}}

@BOOK{HardyWright:2008,
    AUTHOR = {Hardy, G.H. and Wright, E.M.},
     TITLE = {An Introduction to the Theory of Numbers},
 PUBLISHER = {Oxford University Press},
  edition = {6th},
      YEAR = 2008}

@BOOK{FUJIWARA:1929,
    AUTHOR = {Fujiwara, Matsusaburo},
     TITLE = {Algebra, vol. 2 (Japanese)},
 PUBLISHER = {Uchida Rokakuho Publishing Co., Ltd},
  edition = {1st},
      YEAR = 1929}
      
@article{HURWITZ:1893,
author = {Hurwitz, Adolf},
journal = {Mathematische Annalen},
pages = {220--221},
title = {Beweis der Transcendenz der Zahl e},
url = {http://eudml.org/doc/157680},
volume = {43},
year = {1893}
}

@article{Bingham:2011,
  title={Formalizing a Proof that $e$ is Transcendental},
  author={Bingham, Jesse},
  journal={Journal of Formalized Reasoning},
  year={2011},
  volume={4},
  pages={71--84}}

@inproceedings{BernardBRS:2016,
  author = {Bernard, Sophie and Bertot, Yves and Rideau, Laurence and Strub, Pierre{-}Yves},
  editor = {Jeremy Avigad and Adam Chlipala},
  title  = {Formal proofs of transcendence for e and pi as an application of multivariate
             and symmetric polynomials},
  booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
                  and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
  pages = {76--87},
  publisher = {ACM},
  year = {2016},
  url  = {https://doi.org/10.1145/2854065.2854072}
}

} 
