Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar

TL;DR

This paper introduces MizAR, an online service integrating automated reasoning and proof presentation tools with the Mizar system, facilitating formalized mathematics with a focus on human-readable language and leveraging a large mathematical library.

Contribution

It presents MizAR, a novel online platform combining automated reasoning with proof presentation in Mizar, tailored for human mathematicians and utilizing extensive existing mathematical knowledge.

Findings

MizAR effectively integrates automated reasoning with Mizar for formal mathematics.

The system leverages the large Mizar Mathematical Library for improved reasoning.

MizAR enhances proof presentation and accessibility for mathematicians.

Abstract

This paper presents a combination of several automated reasoning and proof presentation tools with the Mizar system for formalization of mathematics. The combination forms an online service called MizAR, similar to the SystemOnTPTP service for first-order automated reasoning. The main differences to SystemOnTPTP are the use of the Mizar language that is oriented towards human mathematicians (rather than the pure first-order logic used in SystemOnTPTP), and setting the service in the context of the large Mizar Mathematical Library of previous theorems,definitions, and proofs (rather than the isolated problems that are solved in SystemOnTPTP). These differences poses new challenges and new opportunities for automated reasoning and for proof presentation tools. This paper describes the overall structure of MizAR, and presents the automated reasoning systems and proof presentation tools that are combined to make MizAR a useful mathematical service.