The goal of Metamath project is to build a framework for formalized mathematics. On the one hand it must be verified automatically, on the other hand a human might want to dive into familiar formalism. One may compare Metamath to Principia mathematica. Let's describe the ideas behind the project.
If we follow the tradition and take widely known first order set theory, namely ZFC, as a foundation, we will fail soon. Why? ZFC and first order languages "as is" are not suitable for a computer to verify as well as for a human to read. In the talk we consider different solutions for these obstacles and how they adopted by Metamath project.
In the second part of the talk we will gradually shift from the very basic notion of class to the very abstract notion of category. On this way we consider familiar concepts of ordinals, relations, functions, numbers and algebraic structures.
Presenter: Kirill K. Smirnov
State University, Stary Peterhof, Universitetski pr., 28