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

[tchow]

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