Abstract

The Mizar Mathematical Library is one of the largest collections of machine understandable formal proofs encompassing many areas of today mathematics including results from algebra, analysis, topology, and lattice theory. The Mizar system has so far been the only tool able to completely process, certify, and make use of these developments. In this paper, we present the progress in the development of an independent certification mechanism of Mizar proofs based on the Isabelle logical framework. The approach allows rechecking the Mizar formal proofs based on a more succinct and more precisely specified formal infrastructure. Additionally, it necessitates a full formal specification of the mechanisms that ensure the correctness of the defined objects, in particular, the proofs that such mechanisms are correct. The development already covers an important part of the Mizar library foundations. We improve the mechanism for defining Mizar structures and show that it permits simpler validation of proof developments involving such objects. To demonstrate this, we perform a complete translation of the Mizar net of basic algebraic structures including their attributes and certify all the corresponding proofs in Isabelle.

BibTeX

@inproceedings{ckkp-fedcsis17,
  author    = {Cezary Kaliszyk and Karol P\k{a}k},
  title     = {Progress in the Independent Certification of {M}izar {M}athematical {L}ibrary in {I}sabelle},
  booktitle = {Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017},
  pages     = {227--236},
  url       = {https://doi.org/10.15439/2017F289},
  doi       = {10.15439/2017F289},
  editor    = {Maria Ganzha and Leszek A. Maciaszek and Marcin Paprzycki},
  year      = {2017},
}