-3
$\begingroup$

Is it technically possible to check formidable proofs like Mochizuki's using PCP theorem before mathematicians spend time in understanding the mechanics of the proof? If so why have mathematicians not done that as this would have saved time and money let alone being distracted on something that might not yield new insights. Will this paradigm of checking before understanding ever stand in mathematics collectively?

Note this is not just to check IUT. Prior almost famous mistake What is the mistake in the proof of the Homotopy hypothesis by Kapranov and Voevodsky? before Vladimir Voevodsky was convinced of usefulness of proof checkers. There are several important examples and so why are the comments and answers focussed on IUT (I say 'check formidable proofs $\underline{like}$ Mochizuki's'?

$\endgroup$
12
  • 4
    $\begingroup$ Have you tried checking any proofs, using PCP? $\endgroup$ Apr 6, 2020 at 23:28
  • 11
    $\begingroup$ To even attempt this you would have to first convert the natural-language proof into a formal proof candidate. That's a gigantic undertaking, and even for reasonably-well-understood arguments is currently a major task. $\endgroup$ Apr 6, 2020 at 23:56
  • 7
    $\begingroup$ If I am unable or unwilling to clarify one of my proofs enough so that experts in the field can understand it and see that it's right, then I am, a fortiori, unable or unwilling to formalize it or to clarify it enough so that other people can formalize it. $\endgroup$ Apr 7, 2020 at 2:23
  • 6
    $\begingroup$ @VS You're quite right that the situation might change. That would probably require big advances in computing. An analogy: 50 years ago, when I wrote my Ph.D. thesis, I couldn't imagine typing it myself --- on (at best) an IBM Selectric, switching in and out the balls that contained the various symbol sets, etc. Now, I type all my own papers. The difference is TeX and the many packages built on it. I suspect the situation that you want will have to wait for the Donald Knuth of theorem-proving. $\endgroup$ Apr 7, 2020 at 2:31
  • 3
    $\begingroup$ @Blaisorblade : I don't think it would be a waste of time. Mochizuki's group is saying that everything is already clear and the people who disagree are being unreasonable. But if a computer says it doesn't understand, one can't complain that the computer is being disrespectful, so one can't dodge the job of clarification and get away with it. As for funding, the Japanese press has reported that considerable sums of money are going to be invested in IUT soon. $\endgroup$ Apr 8, 2020 at 19:13

1 Answer 1

6
$\begingroup$

As people have noted in the comments, the PCP theorem is a red herring, and it makes no sense to formalize a proof before understanding it.

Nevertheless, one could ask if it is reasonable to request that the group of people who claim to understand Mochizuki's proof (and who believe that it is complete and correct) to formalize the proof using a proof assistant.

Until recently, any such request would have been unreasonable for the simple reason that proof assistants were too cumbersome to use. They probably still are too cumbersome to use, but the technology is steadily getting better, and IMO we're close to the point where formalizing something as complicated as IUT is not out of the question. Of course, it would still take an enormous amount of effort. However, apparently it was reported in the Japanese press (Asahi Shimbun, April 4) that a new research center has been created within Kyoto University to work on IUT, and it has an annual budget of ¥40 million. So there does seem to be funding available for the project, should someone want to take it on.

Under normal circumstances, it would be far easier to resolve issues like this one by having mathematicians talk through the proof than to resort to a proof assistant. But the current circumstances are not normal. The group supporting Mochizuki seems to be taking the stance that everything has already been written down in a perfectly clear manner, and that those who object are being disrespectful. Therein lies a crucial difference between humans and computers: Humans are social creatures, and social rifts can occur that interfere with the allegedly objective nature of mathematics. When the normal process of socializing a proof breaks down, it should indeed be possible in principle for computers to "come to the rescue." The group supporting Mochizuki cannot reasonably claim that a proof assistant is being disrespectful when it complains that it doesn't understand an argument that is presented to it.

I seem to be in the minority among professional mathematicians, but I do think that it is reasonable for skeptics of the proof to request that those who claim to understand the proof, and who want to cultivate a whole new generation of younger mathematicians to pursue IUT, to formalize the proof in a proof assistant. If the proof really is correct and those people really do understand it, then the project should eventually succeed, and when it does, the skeptics should be convinced. On the other hand, if the proof has a huge gap, then eventually those tasked with formalization (I'm imagining graduate students) will be forced to confront it, and it will become increasingly hard for "believers" to make excuses for why the formalization project is stalling.

Conversely, if nobody pushes for a formalization, then I don't see any plausible way to stop millions from being invested into this new Kyoto institute. The people in charge of those funds cannot be expected to understand the actual mathematics. But they should be capable of understanding the argument that I have presented here. If the mathematical community thinks that those funds are being misallocated, then I think convincing those who hold the purse strings that they should demand a formalization is one of the most promising avenues forward.

$\endgroup$
3
  • 4
    $\begingroup$ Well, it would be enough to formalize Corollary 3.12 or just write up its proof in more detail ;). Note that the 40 million ¥ going to the new "center" is around 370K USD, which sounds like enough to support a part time professor plus a grad student or two for a few years, not exactly a sprawling research empire. Giving the IUTT project its own funding might even partly be to free it up from possible skepticism in the regular math program. $\endgroup$
    – none
    Apr 9, 2020 at 0:28
  • $\begingroup$ @none That is what I am thinking. $\endgroup$
    – VS.
    Apr 9, 2020 at 12:06
  • $\begingroup$ Just for the record, I stated a similar opinion on the Foundations of Mathematics mailing list back in January 2018. $\endgroup$ Jun 21, 2021 at 16:43

Not the answer you're looking for? Browse other questions tagged or ask your own question.