[vissi]

Those 600 pages are not so well-formalised to be processed by the computer. If they were, that could be 6000 or more pages. Even a simple statement is a lot more verbose in formal form. Also, this is hard algorithmically, even SAT problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem is NP-complete, verifying a generic proof is a lot harder.