Mochizuki on computer verification of abc
Timothy Y. Chow
tchow at math.princeton.edu
Mon Sep 12 00:14:10 EDT 2022
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
More information about the FOM
mailing list