The checking has nothing to do with AI, despite the (massively funded) marketing done to make you think so. It is based on formal methods/theorem provers.
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.