Don't forget that you would need to put not just Mochizuki's work into a proof checker, but also everything that it depends on. From what I understand, this is

Don't forget that you would need to put not just Mochizuki's work into a proof checker, but also everything that it depends on. From what I understand, this is far too much work to be feasible with currently available proof checkers and changing that would require more than incremental improvements.