Application of Complex Classes to Number Theory

Ziobro, Rafał

doi:10.2478/forma-2025-0016

Abstract

The paper illustrates how the formal framework proposed earlier for complex numbers can be applied to integer and natural numbers, facilitating proofs by means of clusters’ registrations for Mizar adjectives. The contents of the article are closely related to the series of Mizar articles “Elementary Number Theory Problems” (with MML identifiers NUMBER*), but it is not solving any of “250 Problems in Elementary Number Theory” by Wacław Sierpiński book.

References

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.
Search in Google Scholar Back to article
Marco B. Caminati and Giuseppe Rosolini. Custom automations in Mizar. Journal of Automated Reasoning, 50(2):147–160, 2013.
Search in Google Scholar Back to article
Adam Grabowski and Artur Korniłowicz. Implementing more explicit definitional expansions in Mizar. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, Białystok, Poland, July 31–August 4, 2023, volume 268 of LIPIcs, pages 37:1–37:8. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ITP.2023.37.
Search in Google Scholar Back to article
Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153–245, 2010.
Search in Google Scholar Back to article
Artur Korniłowicz. Tentative experiments with ellipsis in Mizar. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Intelligent Computer Mathematics, pages 453–457. Springer Berlin Heidelberg, 2012. doi:10.1007/978-3-642-31374-535.
Search in Google Scholar Back to article
Artur Korniłowicz. Elementary number theory problems. Part III. Formalized Mathematics, 30(2):135–158, 2022. doi:10.2478/forma-2022-0011.
Search in Google Scholar Back to article
Artur Korniłowicz. On rewriting rules in Mizar. Journal of Automated Reasoning, 50(2): 203–210, 2013.
Search in Google Scholar Back to article
Adam Naumowicz. Elementary number theory problems. Part I. Formalized Mathematics, 28(1):115–120, 2020. doi:10.2478/forma-2020-0010.
Search in Google Scholar Back to article
Adam Naumowicz. Dataset description: Formalization of elementary number theory in Mizar. In Christoph Benzmüller and Bruce R. Miller, editors, Intelligent Computer Mathematics – 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pages 303–308. Springer, 2020. doi:10.1007/978-3-030-53518-622.
Search in Google Scholar Back to article
Wacław Sierpiński. Elementary Theory of Numbers. PWN, Warsaw, 1964.
Search in Google Scholar Back to article
Wacław Sierpiński. Teoria liczb. Instytut Matematyczny Polskiej Akademii Nauk, 1950. In Polish.
Search in Google Scholar Back to article
Wacław Sierpiński. 250 Problems in Elementary Number Theory. Elsevier, 1970.
Search in Google Scholar Back to article
James J. Tattersall. The Intriguing Natural Numbers. Cambridge University Press, 2005.
Search in Google Scholar Back to article
Rafał Ziobro. Multiplication-related classes of complex numbers. Formalized Mathematics, 28(2):197–210, 2020. doi:10.2478/forma-2020-0017.
Search in Google Scholar Back to article
Rafał Ziobro. Some remarkable identities involving numbers. Formalized Mathematics, 22(3):205–208, 2014. doi:10.2478/forma-2014-0023.
Search in Google Scholar Back to article
Rafał Ziobro. Fermat’s Little Theorem via divisibility of Newton’s binomial. Formalized Mathematics, 23(3):215–229, 2015. doi:10.1515/forma-2015-0018.
Search in Google Scholar Back to article
Rafał Ziobro. Parity as a property of integers. Formalized Mathematics, 26(2):91–100, 2018. doi:10.2478/forma-2018-0008.
Search in Google Scholar Back to article

Application of Complex Classes to Number Theory

Abstract

Paradigm

My account