Mochizuki on computer verification of abc

[Timothy Y. Chow]

On Sun, 11 Sep 2022, Rob Arthan wrote:
> I think it is an over-simplification to say that the assertion that 
> “someone who does not understand the proof might nevertheless guide the 
> proof assistant to a successful conclusion” is nonsensical. Most 
> large-scale problems are solved by teams of individuals, of whom most 
> don’t understand the big picture.  This is standard in engineering and 
> the flyspeck project shows that it applies in formally verified 
> mathematics too

I don't disagree with your last two sentences, so I guess I wasn't clear 
enough about what I was claiming made no sense.

Some of the less informed commentators on machine verification seem to 
think that all that needs to be done, more or less, to achieve a machine 
verification of Mochizuki's purported proof is for someone---anyone---to 
sit down and type Mochizuki's manuscript into Coq.  This of course makes 
no sense.  The team that does the verification must *collectively* have 
some understanding of how the proof is supposed to go.  This is even more 
essential when, as in this case, there is a crucial step of the proof that 
is highly controversial.  There's no way that such a controversy can be 
settled by a team of code monkeys---who jointly have zero understanding of 
how the argument for the controversial claim is supposed to 
go---transcribing Mochizuki's papers line by line into a proof assistant. 
It can be settled only if the side who claims to understand the proof 
drives the formalization.

Tim