Ask HN: Why can't computer verify Mochizuki's proof of ABC conjecture?

I'm not mathematician, but I remember from my logic classes that proof in mathematics is very well defined: it consists of either axioms or their consequences according to set of inference rules.

I understand that it is very hard for computer to generate such a proof, but shouldn't it be very easy to check if proof is correct?

I've recently read an article about Mochizuki's proof and all the controversy, discussions and lack of understanding by community.

Beside it's huge volume (~600 pages) and huge work necessary to transform it to format understandable by appropriate software - are there any other reasons that prevent automatic verification of that proof?

(for those who don't know what I'm writing about: https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/)