Abstract
Representation and management of formalized mathematical knowledge. Large libraries of formalized mathematics, authoring formalized mathematics.
Data mining in formalized mathematics. Proof checking and theorem proving over large libraries of formalized mathematics.