Generalisation of Eisenstein Criterion in Interactive Theorem Prover Mizar
Leonardus Reinaldy Christianto (a), Irawati (b)

(a) Master of Teaching of Mathematics, Bandung Institute of Technology
Jalan Ganesha 10, Bandung 40132, Indonesia
leonardusrenaldi[at]gmail.com
(b) Mathematics, Bandung Institute of Technology
Jalan Ganesha 10, Bandung 40132, Indonesia
irawati[at]itb.ac.id

Abstract

Technological developments offer digitization in various aspects that aim to make it easier for users to access it. One example of digitization currently being developed in the field of mathematics is the interactive theorem prover program - Mizar. Mizar is one of the technological developments designed for mathematicians to verify proofs and document them in the Mizar Mathematics Library. It is intended that a collection of documented articles can become a modern digital encyclopedia in the field of mathematics. Mizar was first introduced in Poland in 1973 and is currently being developed in Japan and China, while in Indonesia there are still not many people who know about the Mizar program. So, in this study, the Mizar program will be introduced along with an explanation regarding the steps to operate it. This research is also part of the author^s experience when working with Mizar in verifying the accuracy of the proof of the generalization of the Eisenstein criterion theorem.

Keywords: Mizar, Application, Program, Mathematics

Topic: COMPUTATIONAL SCIENCES