As people have noted in the comments, the PCP theorem is a red herring, and it makes no sense to formalize a proof before understanding it.
Nevertheless, one could ask if it is reasonable to request that the group of people who claim to understand Mochizuki's proof (and who believe that it is complete and correct) to formalize the proof using a proof assistant.
Until recently, any such request would have been unreasonable for the simple reason that proof assistants were too cumbersome to use. They probably still are too cumbersome to use, but the technology is steadily getting better, and IMO we're close to the point where formalizing something as complicated as IUT is not out of the question. Of course, it would still take an enormous amount of effort. However, apparently it was reported in the Japanese press (Asahi Shimbun, April 4) that a new research center has been created within Kyoto University to work on IUT, and it has an annual budget of ¥40 million. So there does seem to be funding available for the project, should someone want to take it on.
Under normal circumstances, it would be far easier to resolve issues like this one by having mathematicians talk through the proof than to resort to a proof assistant. But the current circumstances are not normal. The group supporting Mochizuki seems to be taking the stance that everything has already been written down in a perfectly clear manner, and that those who object are being disrespectful. Therein lies a crucial difference between humans and computers: Humans are social creatures, and social rifts can occur that interfere with the allegedly objective nature of mathematics. When the normal process of socializing a proof breaks down, it should indeed be possible in principle for computers to "come to the rescue." The group supporting Mochizuki cannot reasonably claim that a proof assistant is being disrespectful when it complains that it doesn't understand an argument that is presented to it.
I seem to be in the minority among professional mathematicians, but I do think that it is reasonable for skeptics of the proof to request that those who claim to understand the proof, and who want to cultivate a whole new generation of younger mathematicians to pursue IUT, to formalize the proof in a proof assistant. If the proof really is correct and those people really do understand it, then the project should eventually succeed, and when it does, the skeptics should be convinced. On the other hand, if the proof has a huge gap, then eventually those tasked with formalization (I'm imagining graduate students) will be forced to confront it, and it will become increasingly hard for "believers" to make excuses for why the formalization project is stalling.
Conversely, if nobody pushes for a formalization, then I don't see any plausible way to stop millions from being invested into this new Kyoto institute. The people in charge of those funds cannot be expected to understand the actual mathematics. But they should be capable of understanding the argument that I have presented here. If the mathematical community thinks that those funds are being misallocated, then I think convincing those who hold the purse
strings that they should demand a formalization is one of the most promising avenues forward.
