3 ms·
There is a major difference though: Holmes's proof was broadly comprehensible, just extremely complicated and easy to get lost in the details. In particular Hol
by nicklecompte 2y ago
There is a major difference though: Holmes's proof was broadly comprehensible, just extremely complicated and easy to get lost in the details. In particular Holmes really tries to make the reader understand, with a fairly gentle/apologetic introduction.
But Mochizuki's "proof" is completely impenetrable even to experts on, like, page 3, and makes no effort to explain what is happening.
Another key difference is that New Foundations is a niche field, so there simply was not a huge amount of human effort spent reading Holmes's work. That's not the case with Mochizuki's proof. There's a big difference between "a small number of mathematicians didn't understand the proof but suspect it's correct" and "a large number of mathematicians didn't understand the proof and concluded it was incorrect."
And, most of all: Holmes's formulation of twisted type theory made the proof a natural candidate for dependently-typed formal verification. Mochizuki's proof is not type-theoretic and does not seem like a great candidate for the calculus of constructions - maybe it is! I actually have no idea. I suspect Mochizuki is the only person in the world who can answer that. But it's critical that Holmes did so much background work to simplify his proof and make this Lean program possible. Mochizuki should do the same.
AFAICT, both in terms of the "sociology of mathematics" and the amount of work required to even attempt a Lean formalization, trying to verify Mochizuki's proof is a waste of time.
- Ericson2314 2y ago> And, most of all: Holmes's formulation of twisted type theory made the proof a natural candidate for dependently-typed formal verification. I am not so sure about this, actually. "twisted type theory" looks like type theory more in the original Bertrand Russel sense than in the modern (Martin Loef, Jean-Yves Girard, etc.) sense.
- alreadydone 2y agoI think TTT stands for "tangled type theory".
- randallholmes 2y agoIt does, but I rather like "twisted type theory" :-)
- nicklecompte 2y agoOops! Good catch. I'm not an expert - I read "tangled type theory" once and "TTT" about 75 times....
- ducttapecrown 2y agoKirti Joshi from the IAS has made very serious attempts to patch up Mochizuki's work by developing new math and by making the exposition good. If you're an expert in arithmetic geometry presumably he's readable, if you're just interested, I found it fun to skim.
- alreadydone 2y agoLatest update here: https://www.math.columbia.edu/~woit/wordpress/?p=13895 https://www.math.columbia.edu/~woit/wordpress/?p=13895 Unfortunately it seems Mochizuki and Scholze reached consensus that a part of Joshi's argument cannot possibly work.
- Davidzheng 2y agoNo comments on the correctness of his work (plenty of discussions online e.g on MO) but why do you say he's from IAS?
- ducttapecrown 2y agoI write about his work on this website to bring notice to his work, because I don't believe Scholze and I'm not going to read Mochizuki (If I did, it would be his original actual contribution to algebraic geometry (and I don't know why I don't read Scholze but its scary mmkay)). So I mentioned that Joshi was from the IAS for the same reason, to convince my readers to read his work. Further edit: I guess he's at Arizona right now, but he was at IAS at some point....