Mochizuki on computer verification of abc

[Rob Arthan]

Tim,

There have been a few arguments about whether machine verifications have actually achieved what. was claimed, but not, as far as I know, in mathematical applications (apart perhaps, from some bickering a few years ago about the Mutilated Chessboard problem by Huet, Paulson myself and others, but that isn’t in the same league as abc).

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

Regards,

Rob.

> On 10 Sep 2022, at 00:41, Timothy Y. Chow <tchow at math.princeton.edu> wrote:
> 
> 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