Mizar a HOL Light jsou dva systemy pro vyvoj formalnich matematickych teorii a jejich pocitacove overovani. Tyto systemy maji ruzne vyhody a nevyhody. HOL Light byl prof. Thomasem Halesem zvolen pro formalizaci jeho nedavneho velmi rozsahleho a vypocetne narocneho dukazu Keplerovy domnenky, ktery lidsti matematici zatim nedokazali plne overit. Mizar je system s rozsahlou knihovnou vet a mnoha aktivnimi autory formalni matematiky. Cilem teto prace je propojit oba systemy tak, aby vety a dukazy vytvorene v jednom systemu mohly byt automaticky prelozeny do vet a dukazu v druhem systemu, coz umozni spolupraci na velkych projektech typu formalizace dukazu Keplerovy domnenky.
Preliminary scope of work in English
Mizar and HOL Light are two systems for formalization of mathematical theories and their computer verification. The systems have different advantages and disadvantages. HOL Loight was chosen by prof. Thomas Hales for formalization of his recent large and computationally involved proof of the Kepler's Conjecture. This proof has not been fully verified yet by other human mathematicians, despite several years of efforts. Mizar is a system with a large library of theorems and many active authors. The goal of this work is to create a link between the two systems, so that theorems and proofs created in one of them could be automatically translated to the other system. This will make cooperation on large projects like the formalization of the proof of Kepler's Conjecture possible.
