[FOM] News about Mochizuki's claimed proof of abc

[Joe Shipman]

There’s an intermediate situation, where PART of the proof requires a bunch of tedious verifications with no real “ideas” explaining “why”, but where that part can be carried out by an algorithm, and where the proof of the algorithm’s correctness DOES qualify as being “understandable”, but the proof as a whole has not been reduced to proof-assistant-checkable form.

The Four Color Theorem is the first and best known example, but since then there have been many others.

The red flag with Mochizuki‘s work is not simply that it is just “one step after another”, but that there are no intermediate results or concrete examples or quantitative bounds which could provide some evidence that the whole structure fits together sensibly. (If there are, they have not been well publicized!)

— JS

Sent from my iPhone

> On Jan 13, 2018, at 9:14 AM, tchow <tchow at alum.mit.edu> wrote:
> 
> For those who have not heard, there is some recent (December 2017) news about the abc conjecture that is somewhat relevant to the current discussion about the reliability of current mechanisms for verifying the correctness of complicated, informally presented proofs.
> 
> Somehow, perhaps as a result of incautious use of Google Translate, a false rumor arose that Mochizuki's claimed proof of the abc conjecture had been accepted for publication.  Perhaps because of this rumor, some number theorists came out publicly with a specific criticism that had been circulating privately, namely that a particular corollary was insufficiently justified:
> 
> https://galoisrepresentations.wordpress.com/2017/12/17/the-abc-conjecture-has-still-not-been-proved/#comment-4619
> 
> As far as I am aware, there has not yet been a satisfactory response to this criticism, although Ivan Fesenko has responded with a few comments:
> 
> https://www.facebook.com/ivan.fesenko.37/posts/1128469910617882
> 
> The discussion surrounding these recent developments has prompted some mathematicians to spell out in some detail their understanding of the existing safeguards for ensuring that complicated but erroneous proofs of important results are not unthinkingly accepted as being correct by the mathematical community.  Namely, before an important result is accepted, the mathematical community has to understand *why* the proof works, in the sense of being able to absorb the main new ideas and apply them to produce new results.  The usual reason why a longstanding open problems remain open for a long time is that there are numerous well-understood conceptual obstacles that any correct proof must be able to circumvent, and the conventional wisdom is that any correct proof must contain *ideas* that break through these barriers.  Confidence in the correctness of the proof arises when these ideas are disseminated and digested and people are able to reconstruct the proof for themselves.
> 
> Now, in principle it could be possible that a correct proof involves no such "ideas" but simply proceeds one trivial step at a time towards the final destination.  The interesting thing about abc is that Mochizuki and others are claiming that this is exactly what is going on with his claimed proof.  Part of people's skepticism is that (they claim) this would be unprecedented in mathematics.
> 
> Finally, I want to make a few remarks about proof assistants.  (These remarks will be obvious to most FOM readers but I include them here in case other readers find themselves reading this.)  Peter Scholze complains that the comments people are making about proof assistants are misguided and irrelevant.  I'll start by saying that I certainly agree that, given that proof assistants are still not very user-friendly (by the standards of the average mathematician), it is unreasonable in 2018 to *demand* that authors of a new, groundbreaking proof produce a formalized version of their argument.  However, suppose we imagine that proof assistants become extremely easy to use.  Then the current situation is exactly the kind of situation where they could be useful in breaking a political stalemate.  We currently have two communities, a small Community A that insists that a proof is correct, and that a particular step that the larger Community B thinks is troublesome is in fact obvious.  If proof assistants are extremely easy to use then Community B can fairly insist, "Well, if it's so trivial, then explain the argument to the proof assistant!"  Community A cannot fairly say, "Proof assistant, your refusal to accept our explanation is offensive and violates etiquette; you must abide by our sociological rules for discipleship and entry into our community."  Conversely, if Community A *does* produce a proof that the proof assistant accepts, then Community B cannot reasonably maintain that the proof is not correct (unless they have cogent objections about the specific proof assistant).  Either way, the deadlock should be broken.  I'm not sure what Scholze's objection is, but it sounds like he's pointing out that Community *B* cannot be reasonably be expected to use a proof assistant to fill a perceived gap in the proof.  This observation is correct, of course, but it seems irrelevant to me.  The point is that Community *A*, who claims that the step *is* trivial, should be able to explain the step to the proof assistant.
> 
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom