Abstrakt
Zvaná přednáška a článek na workshopech KEAPPA a IWIL při konferenci LPAR'2008. Článek podává přehled o existujícím propojení mezi projektem Mizar pro formalizaci matematiky, a nástroji pro automatické uvažování (a zejména automatické dokazování vět). Vysvětluje motivaci pro tuto práci, podává přehled překladových metod a přehled projektů a experimentů založených na tomto propojení.
Dále diskutuje možné budoucí projekty a směry výzkumu v této oblasti.