Mochizuki on computer verification of abc

[Timothy Y. Chow]

I expect that most FOM readers would agree with the following statement, 
or something like it:

   (*) If I have a correct mathematical proof of a theorem, then in
       principle I could code it up in a proof assistant such as
       Mizar/Coq/Isabelle/etc. and the computer would confirm that my
       proof is correct.

There is, of course, always going to be some question of whether what the 
computer-verified theorem accurately captures what the human mathematical 
community is thinking.  So far, though, this "gap" does not seem to have 
caused too much trouble in practice.  Claims of the form, "The proof of 
Theorem X has been verified by machine" have not, to my knowledge, been 
challenged by counterclaims that "What the machine has verified is not 
actually Theorem X," at least not when Theorem X is a well-known result.

The controversy surrounding Shinichi Mochizuki's claimed proof of the abc 
conjecture has led some people to ask whether proof assistants could play 
a role in resolving the disagreement.  Strangely, I sometimes see 
suggestions that someone who *does not understand the proof* might 
nevertheless guide a proof assistant to a successful conclusion.  This of 
course makes no sense.  The only plausible scenario would be for Mochizuki 
to accept the statement (*) above, and to support some kind of formal 
verification effort, much as Scholze supported the Liquid Tensor 
Experiment (i.e., Mochizuki wouldn't have to write any code, but would 
provide a team with mathematical guidance).  Then one would hope that

- if Mochizuki really has a correct mathematical proof, then the team 
would eventually produce a formal proof, and convince skeptics, or

- if there is an unfixable gap in Mochizuki's argument, then he and his 
team would be forced to confront it in the course of the project, and 
could not dismiss the problem with an ad hominem attack.

Such a scenario has of course always been unlikely, but anyone who has 
retained some small glimmer of hope that it might happen one day will be 
dismayed by Section 1.12 (starting on page 29) of the following document 
by Mochizuki, dated July 2022:

https://www.kurims.kyoto-u.ac.jp/~motizuki/Essential%20Logical%20Structure%20of%20Inter-universal%20Teichmuller%20Theory.pdf

I won't claim to understand in detail everything that Mochizuki says in 
this section, but it seems to amount to this: "If you don't understand my 
theory then you're not going to be able to formalize it."  Well, yes, of 
course; as I noted above, it is strange that anyone would think otherwise. 
But that's not the main question.  The question is whether Mochizuki would 
be willing to support something akin to the Liquid Tensor Experiment. 
Though he does not address that question directly, what he *does* say 
makes it seem highly unlikely that he would be willing.  His conception of 
computer verification seems hopelessly out of date:

   [In] situations involving routine numerical computations or manipulation
   of data in some relatively simple combinatorial framework [such as a
   finite group, a finite simplicial complex, or a finite chain of Boolean
   operators] --- computer verification can indeed function as a meaningful
   tool for the verification of mathematical assertions.

Still, perhaps not all hope is lost.  If more junior mathematicians who 
are on good terms with Mochizuki start to formalize some aspects of IUTT, 
then Mochizuki might eventually come around to recognizing that formal 
verification of his proof ought to be possible if his proof is correct. 
If he sincerely believes in the correctness of his proof---which in my 
opinion he does---then perhaps someday he might assent to supporting a 
formal verification project.

Tim