Matematyka w komputerze: Udzial UwB w budowaniu skomputeryzowanej  encyklopedii matematyki. (A.Trybulec)

Język Mizar jest to język formalny, w którym można zapisywać teksty matematyczne tak, aby były jednocześnie czytelne dla człowieka, jak i dla komputera. Pozwala to w szczególności na komputerowa kontrole poprawności dowodów matematycznych pisanych przez człowieka.
    Oprogramowanie sprawdzające poprawnośćć tekstów matematycznych pisanych w Mizarze jest użytecznym narzędziem dydaktycznym. Pozwala ono, dzięki kontroli komputerowej na samodzielna prace ucznia, czy tez studenta. Na naszej uczelni jest używane przy niektórych pracach magisterskich.
    Od 1989 roku jest realizowany międzynarodowy projekt zgromadzenia sprawdzonej przez system wiedzy matematycznej. Poza Polska uczestniczą w nim Japonia, Kanada, Niemcy, Rosja, Holandia, Hiszpania i Chiny. W ciągu 10 lat zgromadzono ok. 600 artykułów napisanych w Mizarze, w których wprowadzono kilka tysięcy definicji i udowodniono dwadzieścia kilka tysięcy twierdzeń.
    Artykuły pisane w języku Mizar są tłumaczone automatycznie na język angielski i publikowane na WWW w czasopiśmie elektronicznym Journal of Formalized Mathematics.