Abstract
This paper gives an overview of the existing link between the Mizar projekt for formalization of mathematics and Automated Reasonig tols (mainly the Automater Theorem Provers (ATPs)). It explains the motovation for this work, gives an overview of the translation method, discusses the projects and works that are based on it, and possible future projects and directions.