- James Douglas Boyd has recently spent a lot of time interacting with Mochizuki and others at RIMS working in anabelian geometry. Material from interviews he conducted are available here (Mochizuki on IUT) and here (on anabelian geometry at RIMS). He also has written a summary of IUT and of the basic problem with the abc proof. These include detailed comments on the issue pointed out by Scholze-Stix and why this is a significant problem for the proof. I’d be curious to hear from anyone who has looked at this closely about whether they agree with Boyd’s characterization of the situation.
There’s also a lot of material the IUT ideas, independent of the problematic abc proof, and about what Mochizuki and others are now trying to do with these ideas.
- Videos from the talks at the conference last month in honor of Manin are now available here. I was especially interested in Dustin Clausen’s talk on Weil groups and ideas about how to go beyond the conventional definition to get something more satisfactory. The twistor line makes an appearance.
- From a story in today’s Wall Street Journal about Woody Allen and his new novel:
Though he’s already at work on a second novel, he rarely reads fiction—“I feel like I’m wasting time.” More often he reads philosophy and books by physicists. “I keep thinking I’m going to learn something of deep value that’s going to make me feel better in life,” he says. “It never does.”
Update: A commenter points to this from Mochizuki, which denounces Boyd and his report, as well as discussing prospects for formalizing IUT and the abc proof.
Update: Kirti Joshi has a new FAQ about the proof of the abc-conjecture. He has also sent me this letter, which more about his view.
The report by JDB reads to me as quite garbled, though perhaps this is inevitable given the subject matter. I think it unfortunately gives the impression that the disagreement comes down to some question about philosophy of mathematics, rather than simple correctness/completeness.
Woody Allen’s comment is hilarious and actually sums up most of my discussions about physics with non-physicists. Most of them very earnestly ask for a bit of deep insight that can illuminate how they feel in their lives, and I can never quite deliver that. As fascinating as physics is with regards to how the outside world functions, it doesn’t seem to have any bearing on our inner lives. It’s heartbreaking because I know exactly where they are coming from, I would love to have found such wisdom, both for my own use and for others. I wonder if it’s the same for other physicists.
This part of Mochizuki’s claim always mystifies me. He claimed this back in the early 2000s. But it’s a complete non-starter. Number theory still works with the axiom of foundation removed. If you are somehow accidentally setting up your theory so that your mathematical objects (in this case, fields, topological groups, categories, etc) are in danger of defining a loop in the ∈-relation, then you are doing it wrong. This feels like Pierre Samuel’s book on algebra where the distinction between the natural numbers constructed via axioms of set theory and the natural numbers inside the reals is keenly felt, and so a “theorem” is proved that you can remove the subset of the reals and replace it by the original set of natural numbers, and get an isomorphic ring (and in fact this is done as a general result, and applied recursively from the complex numbers down through R, Q, Z and N). No one cares about this, and Mochizuki’s fears are even less well-founded (😏 ).
Also, the phrase “inter-universal” is meaningless unless you specify what “universe” is being referred to: actual Grothendieck universes? Something about toposes as places where you can do all of mathematics? Or the fluffy “universe” that is the metaphor for things like “alien ring structure”? I tried to make this point in this post where I quote Mochizuki using “universe” in a variety of conflicting ways.
The different labels thing is again a complete non-starter, and Mochizuki is so hung up on this it’s like an obsession. It’s like the issue with Samuel’s book mentioned above. It’s like worrying that you and I need to label our respective copies of the complex numbers with our names otherwise things might go wrong. Not to toot my own horn, but for people new to this, I also wrote something about this too. Now bringing in some kind of “different universes” machinery when one is literally trying to write down some (countable, even) indexing diagram for a functor is bananas. I don’t know if this is verbatim what Mochizuki told the author of the report, but it’s really not meaningful.
And this is just plain false:
You cannot of course use ZFC to prove such cardinals exist, but you can’t prove they don’t exist in a model of ZFC.
Is this Aurélien Bellanger the writer commenting above, or is there also by chance a physicist named Aurélien Bellanger?
Pascal,
From the email associated with the comment, I’m assuming “Aurélien Bellanger” is being used as a pseudonym.
I really do not understand the goal of the report by JDB. First, he aknowledges that the simplification by Scholze and Stix yields a contradiction in Mochizukis work. What follows is a discussion about if you do label removal this way it works, and that way it doesn’t. This is not helpful. As DL plainly put it im comment #1, it is not “some question about philosophy of mathematics”.
To cite a comment from Scholze from 2020 here again: “I may have not expressed this clearly enough in my manuscript with Stix, but there is just no way that anything like what Mochizuki does can work. (…)”
https://www.math.columbia.edu/~woit/wordpress/?p=11709&cpage=1#comment-235940
And that’s it. Nothing has changed since then. Noone came forward with any new arguments. That JDB mentions twice in his report that Stix is working in a colaboration with people close to RIMS is also not an argument in favor of IUT in my opinion.
mnmltype,
I think JDB’s goal is simply to try and understand what is going on, and write this understanding up in a way that would be helpful for anyone else with such an interest. In particular, he seems to me to have done a great job of explaining Mochizuki’s thinking (Mochizuki’s own attempts to explain himself and to answer criticism of the abc proof have been highly problematic and unconvincing).
His evaluation of the abc proof seems to me to be that the Scholze/Stix criticism is pretty deadly to the proof, while at the same time giving a plausible account of how Mochizuki thinks he can get around it, and why most mathematicians find this unconvincing. He’s clearly skeptical of the abc proof, thinks that possible justification for the new structures Mochizuki introduces will have to come from other directions.
It is rare but not unheard of for serious mathematicians to erroneously convince themselves that they’ve proven something interesting, an post a paper making an (incorrect) claim to this effect. I’ve pointed out maybe 8-10 errors of this nature over the past 10 years. Typically, pointing this out is met with, perhaps, a couple of days during which the authors believes I’ve misunderstood the issue, followed by agreement that there is some gap. Usually the author spends a couple of months trying to fix the gap (unless I’ve found a counterexample to the claimed statement itself) after which the authors will graciously admit the error and retract the claim. As difficult as this sort of situation is, typically mathematicians are able to get past the ego threat and correct their mistakes pretty quickly.
With IUT it has now been 10 YEARS. At this point we should treat the situation as at best common crankery, and at worst, fraud. Substantial monetary prizes have been awarded to nonsense work in the area. It does not speak well of us that this has, apparently, not been communicated to the public. While I guess the drama is fun to discuss, I have very little patience for yet another article suggesting the question of the completeness/correctness of the claimed IUT proof of abc is still open.
DL,
I read this differently. The author says he is trying to explain “why the abc proof strategy will likely not be accepted, but why some arithmetic geometers who don’t care about abc still learn IUT.” About the proof, he’s trying to reproduce what Mochizuki tells him about how he can avoid Scholze/Stix, and concludes with “Nonetheless, I think most mathematicians view the ease with which an immediate contradiction can be derived from the setup as a sign to move on.” It seems clear that his evaluation is that Mochizuki does not have a proof acceptable to other experts in the field.
There is a very good argument to be made that everyone should just ignore the failed abc proof. I’ve mostly done so myself, turning down multiple requests from people that I write about some “news” about it. When I heard about these articles I thought it was a bit interesting. There’s a lot of curiosity about this story. Experts shouldn’t be wasting their time delving into the details of the failed proof and writing comprehensible explanations of what the exact story is for the general public. But if a non-expert wants to spend a lot of his time on a serious effort to do this, I don’t see the problem.
Cannot post to Pet Peeves where it belongs, but preprint below is right on, I think (in case you missed it)
https://arxiv.org/pdf/2509.20929
Severin Pappadeux,
Thanks, I had somehow missed that. I added a link to it as an update on that older post.
I am glad that Boyd put in the effort to interview Mochizuki and write this report. I don’t have the expertise to comment on much of it, but I can say something about the brief section on Lean.
If Mochizuki has a correct proof of abc that uses nothing stronger than ZFCG, then anyone who both understands that proof and is proficient with Lean will be able to formalize a proof of abc in Lean. That would instantly settle the main controversy. There might be some residual debate about some details of the formalization (identification, labels, blah blah blah) but these would be an irrelevant side show. There is no need to reach agreement on the “right” way to formalize these details when a proof of abc is staring you in the face.
Having said that, I’m not optimistic that Lean or any other proof assistant will lead to a resolution of the controversy any time soon. First of all, if Mochizuki’s argument has an unfixable gap but he does not acknowledge it, then he can always take the stance that the failure to produce a formal proof of abc is traceable to the incompetence of the would-be formalizers and/or the inadequacy of Lean. Short of a formal DISPROOF of abc, which I don’t think anybody believes exists, there is nothing you can generate with a proof assistant that can refute such a stance. This is something that a lot of people don’t seem to understand: there is no way you can formally prove that someone who claims to have a proof is bluffing; all you can do is formally disprove a flagship claim. If the flagship claim is true then formal methods cannot definitively rule out the possibility that a particular piece of human-generated text gives all the key ingredients for a proof, for anyone sufficiently intelligent to understand it.
Secondly, even if Mochizuki’s argument is correct, Mochizuki (or someone who agrees with Mochizuki) has to agree that formalizing the proof is a feasible and worthwhile project. There has been no sign of anyone on “Mochizuki’s side” taking this point of view.
If someone were to offer several million dollars to support formalizing a proof of abc in Lean, then that might eventually result in a resolution of the controversy. Either the proof would emerge, or the failure to produce a proof after millions of dollars have been spent would eventually make it clear even to non-mathematicians that the emperor has no clothes.
Thank you, Dr. Woit, for sharing my report, and for your comments. I only just recently saw this.
Thanks, everyone, for taking an interest and for your comments.
I’ll say a few things about the goal of this analysis. The piece itself is about my overall take on IUT and what I think can happen from here – that is, my take on abc in particular and on the theory more generally. So, I began with the following question: after spending time reading, and discussing with Mochizuki, the IUT papers and those on related theories (e.g. Hodge-Arakelov, p-adic Teichmüller, absolute anabelian geometry, etc.), do I see any mathematical value?
I begin the analysis with my own concerns regarding the IUT setup (i.e., the log-theta-lattice, prime-strips, theta-link), which is also the focus of Scholze-Stix, whose concerns I share. I describe the issues I see with ∈-loops, prime-strips, and use of universes/labels. (David Roberts also commented in this thread on why he views such aspects of IUT as “non-starters”). I summarize in the analysis many details regarding the design of IUT based on conversations with Mochizuki. But in the analysis I make clear that I have grave doubts regarding the abc proof and am pessimistic regarding its fate in the mathematical community.
Then, I considered a follow-on question: is there anything good that can happen from here? I still have hope that there’s some anabelian geometry that, independent of the abc proof strategy and the IUT setup, can get absorbed by the anabelian geometry and étale homotopy community.
I think it’s very interesting that Mochizuki has said on record that he’s not particularly interested in abc, that colleagues such as Lepage aren’t either, and that they mostly care about anabelian geometry. I think this helps explain why some folks, including the AHGT (CNRS) project organizer, are engaging with Mochizuki.
Why is it worth considering if something good can happen? Because it offers a fresh pathway for productive and collaborative work to be done. I don’t want to see another decade of RCS debates. If folks indifferent to abc spend the next decade talking about mono-anabelian transport or cyclotomic synchronization and why it is useful for their work on GT or some other topic in étale homotopy, that will be better. And that’s already happening.
I definitely don’t write on CNRS/AHGT and prospects for anabelian geometry in order to “open up the question” of the abc proof question again. Rather – and this is what I wrote in my last email to Mochizuki – I very much hope, if he does care about anabelian geometry more than abc, that the abc proof dispute can perhaps be set aside and activity can be more focused on teasing out the anabelian geometry in the IUT papers that seems to be of most interest to many involved.
I also mention this issue of the “algorithms” in the IUT papers, or the term Mochizuki and colleagues use for the anabelian-geometric and reconstruction techniques in the IUT papers. Mochizuki continues to make the argument that Scholze-Stix, by simplifying things down to the basic setup and not using the algorithms, don’t adequately consider IUT in its full scope. I make some arguments about why, with the IUT setup itself problematic, I’m not surprised to see little interest in going deeper to the algorithms.
On the other hand, I think they can be extracted the IUT setup, mostly because they have a different history. I think there is some interest among some mathematicians in the anabelian geometry community in these algorithms. I’m not saying that, because Scholze-Stix don’t discuss the algorithms at length in their manuscript, this interest in the algorithms might “flip the script” on the abc dispute. Rather, I discuss it because, if this interest can tease out the anabelian geometry independently of the IUT setup, then the anabelian geometry might be developed by more people. Something good might happen in anabelian geometry or étale homotopy. Mochizuki belongs to the RIMS anabelian geometry community, which is a marvelous community, which is itself engaging quite deeply with the AHGT network. If some folks who don’t care about abc can still find valuable mathematics among the many constructions at play in the IUT papers, I think that’s a redemptive, positive development.
For those just interested in the abc question, I can appreciate that this analysis might not be of interest: I don’t have anything more firm to say on abc than Scholze-Stix, so there’s little value in that regard. (One might also call some of the views I put forth on the abc proof strategy as being “philosophical”, as they pertain to issues like the Axiom of Grothendieck universes or questions of inconsistency in theories, but I offer these comments to give a summary of my concerns in a broader context.)
After years of drama, I’d still like to see something good come out of the IUT affair, which, I think, will have to be independent of the abc proof strategy; so, I wrote up what I think could happen to make the situation better.
P.S. David Roberts, thank you for pointing out my imprecise wording regarding strongly inaccessible cardinals and ZFC. I changed the wording in the PDF to “whose existence cannot be proven in ZFC” rather than “doesn’t exist in ZFC”. (Though, from a constructivist point of view, these two statements are perhaps not so dissimilar.) Also, when I wrote “it’s not controversial that IUT uses an inter-universal setup to avoid set-theoretic contradictions (which Mochizuki calls “∈-loops”)”, I meant by “not controversial” that no one who knows the history debates that Mochizuki was aware of the ∈-loops implicit in the way the theta-link works and chose to make the theory inter-universal to try to keep them at bay (which is why, in my view, the Scholze-Stix argument shouldn’t come as a surprise.)
my contention is that this is a sign that something has come off the rails. No one outside of axiomatic set theory needs to care about such things turning up. The theory should (I say should) work in different set theory axioms that doesn’t even have a global ∈ relation, if it is sound. Moreover there are set theories (with axioms on a global ∈) where ∈-loops are perfectly harmless. Anabelian geometry for the purposes of studying number fields cannot be so sensitive to the choice of axiomatic approach to sets (ZFC vs ETCS+R vs ZFC+AFA vs ……), ignoring the relatively minor-by-comparison detail of needing to assume the Grothendieck-Tarski universe axiom.
Yes, I agree that the preoccupation with “∈-loops” is a sign that something went awry. I also agree that the “∈-loops” are not the core issue, but they are related.
So, what are these ∈-loops? What Mochizuki and I established during our discussions is that the ∈-loop comes from the way “prime-strips” (as they are called) are treated. (This is also at the heart of the Scholze-Stix critique.) So, the Diophantine goal in IUT is to somehow work with a certain collection of primes (of bad reduction) called “prime-strips” as though they were equivalent to all primes, even though they aren’t. So, this set belongs to the greater set of primes. Treating them as equal is essentially saying that the part is the same as the whole. So, if this set is $p$, and all primes are $P$, then $p \in P$; but here, because IUT setup supposes $p=P$, this implies $p \in p$; that’s the origin of this phrase “∈-loop”, which, in my view, doesn’t really get to the core issue. $p \in p$ is not the real issue; the real issue is that IUT supposes $p=P$ even though $p \neq P$. So, “∈-loops” are kind of just a euphemism for identifications that yield contradictions in IUT.
This is important because, from the beginning (i.e., the early 2000’s, as you mentioned), a key stated motivation for “inter-universality”/distinct labels has been these “∈-loops”, but what that really means is that a key motivation has been treating prime-strips as equivalent to all primes even though they aren’t. This is why, with time, I became very sympathetic to the Scholze-Stix argument: it’s just showing that if you remove the labeling apparatus put in place to suspend the contradiction that ensues from supposing $p=P$, the contradiction manifests immediately.
I use the following analogy to think about this “inter-universal” strategy: it’s like you have a syntax error, but you work with the LHS in one computer and the RHS in another computer so that you don’t get an error message; the universes are like these separate computers. The Scholze-Stix argument, which simplifies everything down to two Hodge theaters and the theta-link, says, essentially, “let’s just run this thing in one computer from the start and see what happens.” The answer is, of course, the syntax error pops up immediately.
I’m curious as to why people are still beating the Mochizuki vs. Scholze & Stix horse, and not the more recent Mochizuki vs. Scholze & Stix vs. Joshi horse.
In May 2025, Kirti Joshi published his “Final Report on the Mochizuki-Scholze-Stix Controversy”, claiming:
– Mochizuki’s original argument has a gap,
– Scholze & Stix’s argument is also flawed, and
– he himself filled in Mochizuki’s gap, completing the proof.
To quote Kirti Joshi:
> […] every assertion of [Scholze and Stix, 2018] and [Scholze, 2021] is mathematically false. On the other hand, Mochizuki’s proof is also incomplete (see § 1.2). A robust version of the theory claimed by Mochizuki is provided by my work.
> At the very center of the issue is that Mochizuki’s quantification of what it means to be an Arithmetic Holomorphic Structure is mathematically inadequate to quantitatively assert that one has two or more such structures.
> Peter Scholze and Jakob Stix recognized this problem (2018) – but they extrapolated and argued (incorrectly) that many such structures cannot exist (see § 1.3).
Source: https://arxiv.org/pdf/2505.10568
Winnie Pooh,
The problem for Joshi is that Mochizuki strongly disagrees with him, as does Scholze. Of the experts I’ve asked, all are pessimistic that Joshi really has a proof. I keep hoping that this will get resolved by the conventional refereeing system: he’ll submit the papers with the proof to a reputable journal, they’ll find one or more willing referees, who will go through his arguments carefully and either show him where they are flawed, or vouch for their soundness.
Until an expert other than Joshi himself has gone through his proof, is convinced it works, and can explain it to others, there seems to me no point to discussing this part of the story among non-experts here on this blog.
Mochizuki’s response to Boyd’s report:
https://www.kurims.kyoto-u.ac.jp/~motizuki/IUT-report-2025-10.pdf
(Feel free to disregard this, as the response contains ad hominem attacks.)
In a comment above, I said that there has been no sign of anyone on “Mochizuki’s side” taking the view that formalizing the proof is a feasible and worthwhile project. Even if this was true at the time, it is not true any more. I just learned that in a recent report, Mochizuki has expressed enthusiasm about a “Lean-style formalization” of IUT (see Section 3.2 in particular). I see this as a very hopeful sign for breaking the deadlock.