>>93

続き
One could challenge Mochizuki, or indeed anyone, to formalise the proof in a computer theorem prover.
However this would be a completely
unreasonablething to do.
A computer formalisation is not expected of other proofs appearing in our literature.
Furthermore, the key sticking point right now is that the unbelievers
argue that more details are needed in the proof of Corollary 3.12 in the main paper,
and the state of the art right now is simply that one cannot begin to formalise this
corollary without access to these details in some form (for example a paper proof
containing far more information about the argument).

What would however be feasible is for mathematicians to formalise parts of
technical work, or to get others to do so. There might be several reasons to do
such a thing – Commelin and his team have already shown that theorem provers24 KEVIN BUZZARD can be used to check parts of complex proofs which humans might find it difficult to plough through, whilst learning about the mathematics in the process

https://arxiv.org/abs/2112.11598