Mochizuki often discusses the IUT papers in algorithmic terms. Few understand IUT, and its abc proof strategy is disputed. So, many – including Charles Hoskinson, after whom the Hoskinson Center for Formal Mathematics at Carnegie Melon is named – have suggested that it be formalized in Lean. My own outlook is that Lean won’t help in this case, since at issue is this matter of label-removals and R-identifications.
Lean admits distinct type-theoretic universes, which, as Carneiro discusses, if viewed in a set-theoretic framework, are indeed Grothendieck universes. So, on the one hand, I can imagine one trying to formalize the multiradial algorithms using type-theoretic universes with “distinct labeling”, perhaps put in by hand. The IUT papers symbolically label the Hodge theaters, q parameters, and other data (e.g., with † or ‡). So, formalizing IUT in a manner consistent with the papers would require encoding labels to prevent data from being identified. One could give them labels, perhaps, with irreducible definitions (or something like that), in order to make them resistant to equivalences. On the other hand, to formalize the Scholze-Stix argument, one would make the data readily amenable to identification.
I don’t foresee Lean being good for resolving a dispute such as this. Whether or not data is identified or kept distinct is a coding choice, just as it is a symbolic choice in pen-and-paper math. I can imagine both sides finding a way to code up their approach, only to dispute their respective approaches.
This matches my broader impression from following formalisation work elsewhere that the locus of dispute wouldn’t necessarily disappear but can shift to whether the formal setup (definitions etc) was done properly, and (as the Mochizuki vs Scholze-Stix example above shows) this dispute can be ~irreconcilable because what Mochizuki may consider essential features of his argument SS consider removable WLOG.
Maybe IUT would face issues in Lean. But Joshi shouldn’t, so formalizing Joshi can be a warm-up for formalizing Mochizuki, and then if IUT truly can’t be formalized in Lean, we’ve learned something.
I think there’s also interest in understanding IUT independently of the abc conjecture. It’s meant to be a whole new “theory” (in the sense of e.g. Galois theory, a body of original concepts pertaining to a particular corner of math), so someone should be interested in understanding how it works. But maybe you have to be an arithmetic geometer to have a chance of doing that.
What are the formalization disputes you know from elsewhere?
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.
I used to think so too, Mochizuki’s strenuous denunciations of Joshi’s work notwithstanding. James Boyd’s contra take gave me pause:
This matches my broader impression from following formalisation work elsewhere that the locus of dispute wouldn’t necessarily disappear but can shift to whether the formal setup (definitions etc) was done properly, and (as the Mochizuki vs Scholze-Stix example above shows) this dispute can be ~irreconcilable because what Mochizuki may consider essential features of his argument SS consider removable WLOG.
Maybe IUT would face issues in Lean. But Joshi shouldn’t, so formalizing Joshi can be a warm-up for formalizing Mochizuki, and then if IUT truly can’t be formalized in Lean, we’ve learned something.
There is, incidentally, a $1M prize for any refutation of Mochizuki’s proof, to be awarded at the discretion of tech & entertainment tycoon Nobuo Kawakami.
I think there’s also interest in understanding IUT independently of the abc conjecture. It’s meant to be a whole new “theory” (in the sense of e.g. Galois theory, a body of original concepts pertaining to a particular corner of math), so someone should be interested in understanding how it works. But maybe you have to be an arithmetic geometer to have a chance of doing that.
What are the formalization disputes you know from elsewhere?
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.