%0 Journal Article %1 korniowicz2017liouville %A Korniłowicz, Artur %A Naumowicz, Adam %A Grabowski, Adam %D 2017 %J Formalized Mathematics %K liouville_number mathematics transcendental_numbers %N 1 %R 10.1515/forma-2017-0004 %T All Liouville Numbers are Transcendental %U https://sciendo.com/article/10.1515/forma-2017-0004 %V 25 %X In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. Liouville numbers were introduced by Joseph Liouville in 1844 15 as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real number x is a Liouville number iff for every positive integer n, there exist integers p and q such that q > 1 and It is easy to show that all Liouville numbers are irrational. The definition and basic notions are contained in 10, 1, and 12. Liouvile constant, which is defined formally in 12, is the first explicit transcendental (not algebraic) number, another notable examples are e and π 5, 11, and 4. Algebraic numbers were formalized with the help of the Mizar system 13 very recently, by Yasushige Watase in 23 and now we expand these techniques into the area of not only pure algebraic domains (as fields, rings and formal polynomials), but also for more settheoretic fields. Finally we show that all Liouville numbers are transcendental, based on Liouville’s theorem on Diophantine approximation.

@article{korniowicz2017liouville, abstract = {In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. Liouville numbers were introduced by Joseph Liouville in 1844 15 as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real number x is a Liouville number iff for every positive integer n, there exist integers p and q such that q > 1 and It is easy to show that all Liouville numbers are irrational. The definition and basic notions are contained in 10, 1, and 12. Liouvile constant, which is defined formally in 12, is the first explicit transcendental (not algebraic) number, another notable examples are e and π 5, 11, and 4. Algebraic numbers were formalized with the help of the Mizar system 13 very recently, by Yasushige Watase in 23 and now we expand these techniques into the area of not only pure algebraic domains (as fields, rings and formal polynomials), but also for more settheoretic fields. Finally we show that all Liouville numbers are transcendental, based on Liouville’s theorem on Diophantine approximation.}, added-at = {2023-10-03T21:31:23.000+0200}, author = {Korniłowicz, Artur and Naumowicz, Adam and Grabowski, Adam}, biburl = {https://www.bibsonomy.org/bibtex/29bc3348138608c490d194e6b363aca7f/tabularii}, doi = {10.1515/forma-2017-0004}, interhash = {3d86bd388d6dd7dd0af79c0a06c5ea03}, intrahash = {9bc3348138608c490d194e6b363aca7f}, journal = {Formalized Mathematics}, keywords = {liouville_number mathematics transcendental_numbers}, number = 1, timestamp = {2023-10-04T15:15:49.000+0200}, title = {All Liouville Numbers are Transcendental}, type = {Publication}, url = {https://sciendo.com/article/10.1515/forma-2017-0004}, volume = 25, year = 2017 }