There's a lot of automated proof checkers out there. Presumably you would just run any solution from an AI through those.