All the mathematicians quoted above can successfully write proofs that convince experts that something is true and why something is true; the quotes are about the difficulty of conveying the way the mathematician found that truth. All those mathematicians can convey the that and and the why — except for Mochizuki and his circle.
The matter of Mochizuki’s work on the abc conjecture is intriguing because the broader research community has neither accepted his proof nor refuted it. The way to bet now is that his proof is wrong:
Professional mathematicians have not and will not publicly declare that “Mochizuki’s proof is X% likely to be correct”. Why? I’d guess one reason is that it’s their job to provide a definitive verdict that serves as the source of truth for probabilistic forecasts. If the experts gave subjective probabilities, it would confuse judgments of different kinds.
Most people with an opinion regard Mochizuki as refuted by Scholze and Stix. They simplified his theory to do it and Mochizuki says they oversimplified, but no one has managed to understand how the details of the full theory would make any difference.
If I was trying to resolve the issue, I might start by formalizing (in Lean) Kirti Joshi’s claimed proof of abc, which is inspired by Mochizuki but which uses more familiar mathematics.
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.
To add nuance to this picture, while you’re right that the broader community has neither accepted nor refuted his proof of the abc conjecture, I just learned from James Boyd’s writeup that there’s been growing interest in his broader work outside of RIMS:
Before explaining the details, I want to make a sudden turn and, setting the fate of abc aside, share a somewhat optimistic point on a different matter. So, I agree that Scholze-Stix are able to make their argument without the algorithms. One might ask if anyone has looked at the math beyond the basics critiqued by Scholze-Stix. The fascinating wrinkle in the story – to talk inside baseball – is that this mathematics is of interest to some mathematicians, and they are engaging with IUT; they mostly come from anabelian geometry and related fields, and – importantly – generally have no interest in abc. It’s sometimes supposed that these mathematicians must just be cajoled students or abc “true believers”, but, in fact, much of the interaction is happening in collaboration with CNRS, the largest science funder in Europe.
What happened is twofold. On the one hand, the abc proof strategy provoked a global controversy. On the other hand, looking at some of the math in the IUT papers and setting aside abc, a relationship between aspects of IUT, anabelian geometry, and related topics such as étale homotopy and Grothendieck-Teichmüller theory did prove attractive to some mathematicians in those areas. …
(there’s a section further down expanding on this)
Yeah the next level of the question is something like “we can prove something to a small circle of experts, now how do we communicate the reasoning and the implications to policymakers/interested parties/the public in general”
All the mathematicians quoted above can successfully write proofs that convince experts that something is true and why something is true; the quotes are about the difficulty of conveying the way the mathematician found that truth. All those mathematicians can convey the that and and the why — except for Mochizuki and his circle.
The matter of Mochizuki’s work on the abc conjecture is intriguing because the broader research community has neither accepted his proof nor refuted it. The way to bet now is that his proof is wrong:
Professional mathematicians have not and will not publicly declare that “Mochizuki’s proof is X% likely to be correct”. Why? I’d guess one reason is that it’s their job to provide a definitive verdict that serves as the source of truth for probabilistic forecasts. If the experts gave subjective probabilities, it would confuse judgments of different kinds.
Most people with an opinion regard Mochizuki as refuted by Scholze and Stix. They simplified his theory to do it and Mochizuki says they oversimplified, but no one has managed to understand how the details of the full theory would make any difference.
If I was trying to resolve the issue, I might start by formalizing (in Lean) Kirti Joshi’s claimed proof of abc, which is inspired by Mochizuki but which uses more familiar mathematics.
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.
To add nuance to this picture, while you’re right that the broader community has neither accepted nor refuted his proof of the abc conjecture, I just learned from James Boyd’s writeup that there’s been growing interest in his broader work outside of RIMS:
(there’s a section further down expanding on this)
Yeah the next level of the question is something like “we can prove something to a small circle of experts, now how do we communicate the reasoning and the implications to policymakers/interested parties/the public in general”