This seems like nonsense. If there’s any way to formalize what Mochizuki claims, he could and should do this to achieve what might be the greatest intellectual upset in history. On the other hand, he’s likely just wrong about something and his proof wouldn’t go through, so there’s no use in trying to settle this with a proof assistant.
Your phrasing seems to assume Mochizuki is the one skeptical of formalisation (the quote is from Boyd, not Mochizuki). Mochizuki himself really wants formalisation and is actively involved in various related efforts, e.g. Section 3.2 of his report (all emphasis his):
I have also been deeply impressed and encouraged by the entirely unanticipated enthusiasm that has been exhibited in recent years by computer scientists deeply involved with the development of Lean who are not mathematicians, and whose work has no direct connections to arithmetic geometry (hence, a fortiori, to IUT!), but who have expressed a keen interest in learning more about the situation surrounding IUT and, in particular, investigating what can be done with regard to pursuing the goal of Lean-style formalization of IUT. Such computer scientists, despite being disconnected from the mathematical community in a strict professional sense, nevertheless have substantial personal interaction with professional mathematicians, and it is through such personal connections that this enthusiasm was communicated to me. Moreover, as a result of these ties between the Lean-development community and the mathematical community, I have been invited to give an online talk on the topic of Lean-style formalization of IUT at a workshop on formalization that has been scheduled to be held in the spring of 2026 in the United Kingdom.
This seems like nonsense. If there’s any way to formalize what Mochizuki claims, he could and should do this to achieve what might be the greatest intellectual upset in history. On the other hand, he’s likely just wrong about something and his proof wouldn’t go through, so there’s no use in trying to settle this with a proof assistant.
Your phrasing seems to assume Mochizuki is the one skeptical of formalisation (the quote is from Boyd, not Mochizuki). Mochizuki himself really wants formalisation and is actively involved in various related efforts, e.g. Section 3.2 of his report (all emphasis his):
I did not know this! And it’s quite an update for me regarding Mochizuki’s credibility on the matter.