The point of the AI with respect to checking is to translate a natural language theorem and its proof into the formal system. Most of known math is not formalized because it is very hard to do so.