REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

  1. Repozytorium Uniwersytetu w Białymstoku
  2. Czasopisma naukowe / Journals
  3. Formalized Mathematics
  4. Formalized Mathematics, 2024, Volume 32, Issue 1

Szukanie zaawansowane
  • Zespoły i Kolekcje


  • Zaloguj się
  • Zarejestruj się
  • Mój RUB
  • FAQ
  • Polityka
  • Regulamin
  • DOI
  • Instrukcja
  • Aspekty prawne
  • Open Access
  • Archiwum


  • Kontakt
  • O Dspace
  • Strona Biblioteki
  • Strona Uczelni



    • Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/17770
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorWatase, Yasushige-
    dc.date.accessioned2024-12-31T07:35:15Z-
    dc.date.available2024-12-31T07:35:15Z-
    dc.date.issued2024-
    dc.identifier.citationFormalized Mathematics, Volume 32, Issue 1, Pages 121–131pl
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/17770-
    dc.description.abstractIn 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.pl
    dc.language.isoenpl
    dc.publisherDeGruyter Openpl
    dc.rightsAttribution-ShareAlike 3.0 Unported (CC BY-SA 3.0)pl
    dc.rights.urihttps://creativecommons.org/licenses/by-sa/3.0/pl
    dc.subjecttranscendental numberpl
    dc.subjectalgebraic numberpl
    dc.subjectring of polynomialspl
    dc.titleFormal Proof of Transcendence of the Number e. Part IIpl
    dc.typeArticlepl
    dc.rights.holder© 2024 The Author(s)pl
    dc.rights.holderCC BY-SA 3.0 licensepl
    dc.identifier.doi10.2478/forma-2024-0009-
    dc.description.AffiliationSuginami-ku Matsunoki 6, 3-21 Tokyo, Japanpl
    dc.description.referencesAlan Baker. Transcendental Number Theory. Cambridge University Press, 1990.pl
    dc.description.referencesGrzegorz 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.pl
    dc.description.referencesGrzegorz 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.pl
    dc.description.referencesSophie 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.pl
    dc.description.referencesJesse Bingham. Formalizing a proof that e is transcendental. Journal of Formalized Reasoning, 4:71–84, 2011.pl
    dc.description.referencesManuel Eberl. The transcendence of e. Archive of Formal Proofs, 2017. https://isa-afp.org/entries/E_Transcendental.html, Formal proof development.pl
    dc.description.referencesMatsusaburo Fujiwara. Algebra vol 2, Japanese. Uchida Rokakuho Publishing Co., Ltd, 1st edition, 1929.pl
    dc.description.referencesAdolf Hurwitz. Beweis der Transcendenz der Zahl e. Mathematische Annalen, 43:220–221, 1893.pl
    dc.description.referencesArtur Korniłowicz. Elementary number theory problems. Part VIII. Formalized Mathematics, 31(1):87–100, 2023. doi:10.2478/forma-2023-0009.pl
    dc.description.referencesArtur 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.pl
    dc.description.referencesArtur 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.pl
    dc.description.referencesSerge Lang. Introduction to Transcendental Numbers. Addison-Wesley Pub. Co., 1966.pl
    dc.description.referencesNorman D. Megill and David A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019.pl
    dc.description.referencesRobert Milewski. Fundamental theorem of algebra. Formalized Mathematics, 9(3):461–470, 2001.pl
    dc.description.referencesLeonardo 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.pl
    dc.description.referencesKarol Pąk. Eigenvalues of a linear transformation. Formalized Mathematics, 16(4):289–295, 2008. doi:10.2478/v10037-008-0035-x.pl
    dc.description.referencesChristoph Schwarzweller. On roots of polynomials over F[X]/hpi. Formalized Mathematics, 27(2):93–100, 2019. doi:10.2478/forma-2019-0010.pl
    dc.description.referencesChristoph Schwarzweller. Normal extensions. Formalized Mathematics, 31(1):121–130, 2023. doi:10.2478/forma-2023-0011.pl
    dc.description.referencesYasushige Watase. Formal proof of transcendence of the number e. Part I. Formalized Mathematics, 32(1):111–120, 2024. doi:10.2478/forma-2024-0008.pl
    dc.description.referencesYasushige 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.pl
    dc.description.referencesFreek Wiedijk. Formalizing 100 theorems. Available online at http://www.cs.ru.nl/~freek/100/.pl
    dc.identifier.eissn1898-9934-
    dc.description.volume32pl
    dc.description.issue1pl
    dc.description.firstpage121pl
    dc.description.lastpage131pl
    dc.identifier.citation2Formalized Mathematicspl
    Występuje w kolekcji(ach):Formalized Mathematics, 2024, Volume 32, Issue 1

    Pliki w tej pozycji:
    Plik Opis RozmiarFormat 
    Formal-Proof-of-Transcendence-of-the-Number-e-Part-II.pdf333,49 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


    Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons