@ARTICLE(MatRud2005,
    AUTHOR  = {Matuszewski, Roman and Rudnicki, Piotr},
    TITLE   = {Mizar: The First 30 Years},
    JOURNAL = {Mechanized Mathematics and Its Applications},
    VOLUME  = {4},
    PAGES   = {3--24},
    YEAR    = {2005},
    NOTE    = {\url{http://mizar.org/people/romat/MatRud2005.pdf})