Es soll für die Sprache Mizar ein Suchprogramm erstellt werden. Das entwickelte Programm nimmt eine Benutzereingabe entgegen, und gibt gefundene Treffer aus. Andererseits kann das Programm aus einem XML-Dokument, das ein Mizar-Theorem enthält, ein Mizar-Beweisrahmen erzeugen.