On the Integrity of a Repository of Formalized Mathematics

  • Piotr Rudnicki
  • Andrzej Trybulec
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2594)


Mizar ,a proof-checking system,is used to build the Mizar Mathematical Library (MML ).This is a long term project aiming at building a comprehensive library of mathematical knowledge. The language and the checking software evolve, and the evolution is driven by the growing library. We discuss the issues of maintaining integrity of an electronic repository of formal mathematics, based on our experience with MML .


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Grzegorz Bancerek.The ordinal numbers.Formalized Mathematics,1(1 ):91–96, 1990.Google Scholar
  2. 2.
    Grzegorz Bancerek. König’s theorem.Formalized Mathematics,1(3 ):589–593, 1990.Google Scholar
  3. 3.
    Grzegorz Bancerek.Cartesian product of functions.Formalized Mathematics, 2(4 ):547–552,1991.Google Scholar
  4. 4.
    Grzegorz Bancerek.Reduction relations.Formalized Mathematics,5(4 ):469–478, 1996.Google Scholar
  5. 5.
    Grzegorz Bancerek.Continuous lattices of maps between T 0 spaces.Formalized Mathematics,9(1 ):111–117,2001.zbMATHGoogle Scholar
  6. 6.
    Grzegorz Bancerek and Krzysztof Hryniewiecki.Segments of natural numbers and finite sequences.Formalized Mathematics,1(1 ):107–114,1990.Google Scholar
  7. 7.
    Czesław Byliński.Some basic properties of sets.Formalized Mathematics,1(1 ):47–53,1990.Google Scholar
  8. 8.
    Czesław Byliński.Functions from a set to a set.Formalized Mathematics ,1(1 ):153–164,1990.Google Scholar
  9. 9.
    Czesław Byliński.Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics,1(3 ):529–536,1990.Google Scholar
  10. 10.
    Czesław Byliński and Piotr Rudnicki.Bounding boxes for compact sets in ⌉2. Formalized Mathematics ,6(3 ):427–440,1997.Google Scholar
  11. 11.
    Agata Darmochwał.The Euclidean space.Formalized Mathematics,2(4 ):599–603, 1991.Google Scholar
  12. 12.
    Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics,1(3 ):607–610,1990.Google Scholar
  13. 13.
    Artur Korniłowicz.Cartesian products of relations and relational structures.For-malized Mathematics,6(1 ):145–152,1997.Google Scholar
  14. 14.
    Jarosław Kotowicz.Convergent real sequences.Upper and lower bound of sets of real numbers.Formalized Mathematics,1(3 ):477–481,1990.Google Scholar
  15. 15.
  16. 16.
    Yatsuka Nakamura and Adam Grabowski.Bounding boxes for special sequences in ⌉2.Formalized Mathematics,7(1 ):115–121,1998.Google Scholar
  17. 17.
    Yatsuka Nakamura and Piotr Rudnicki.Vertex sequences induced by chains.For-malized Mathematics,5(3 ):297–304,1996.Google Scholar
  18. 18.
    Adam Naumowicz and Czesław Byliński.Basic Elements of Computer Algebra in Mizar.Mechanized Mathematics and Its Applications,2 (1):9–16,2002.Google Scholar
  19. 19.
    Beata Padlewska and Agata Darmochwał.Topological spaces and continuous func-tions.Formalized Mathematics,1(1 ):223–230,1990.Google Scholar
  20. 20.
    P. Rudnicki, Ch. Schwarzweller and A. Trybulec.Commutative Algebra in the Mizar System.Journal of Symbolic Computation,32 :143–169,2001.MathSciNetCrossRefGoogle Scholar
  21. 21.
    Piotr Rudnicki and Andrzej Trybulec.On equivalents of well-foundedness.Journal of Automated Reasoning ,23 (3-4):197–234,1999.MathSciNetCrossRefGoogle Scholar
  22. 22.
    Piotr Rudnicki and Andrzej Trybulec.Mathematical Knowledge Management in Mizar.1st Int.Workshop on MKM ,Sept.24–26,2001,
  23. 23.
    Agnieszka Sakowicz, Jarosław Gryko, and Adam Grabowski. Sequences in⌉n tFormalized Mathematics,5(1 ):93–96,1996.Google Scholar
  24. 24.
    Andrzej Trybulec.Tarski Grothendieck set theory.Formalized Mathematics , 1(1 ):9–11,1990.Google Scholar
  25. 25.
    Wojciech A. Trybulec.Non-contiguous substrings and one-to-one.nite sequences. Formalized Mathematics,1(3 ):569–573,1990.Google Scholar
  26. 26.
    Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-Based Finite Sequences. Formalized Mathematics,9(4):825–829,2001.Google Scholar
  27. 27.
    Freek Wiedijk.Mizar:An Impression.

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Piotr Rudnicki
    • 1
  • Andrzej Trybulec
    • 2
  1. 1.Dept.of Computing ScienceUniversity of AlbertaEdmontonCanada
  2. 2.Institute of InformaticsUniversity in BiałystokBiałystokPoland

Personalised recommendations