A few days ago Eric had a post about an insightful text that has been making the rounds on the internet, which narrates the story of a mathematical ‘proof’ that is for now sitting somewhere in a limbo between the world of proofs and the world of non-proofs. The ‘proof’ in question purports to establish the famous ABC conjecture, one of the (thus far) main open questions in number theory. (Luckily, a while back Dennis posted an extremely helpful and precise exposition of the ABC conjecture, so I need not rehearse the details here.) It has been proposed by the Japanese mathematician Shinichi Mochizuki, who is widely regarded as an extremely talented mathematician. This is important, as crackpot ‘proofs’ are proposed on a daily basis, but in many cases nobody bothers to check them; a modicum of credibility is required to get your peers to spend time checking your purported proof. (Whether this is fair or not is beside the point; it is a sociological fact about the practice of mathematics.) Now, Mochizuki most certainly does not lack credibility, but his ‘proof’ has been made public quite a few months ago, and yet so far there is no verdict as to whether it is indeed a proof of the ABC conjecture or not. How could this be?

As it turns out, Mochizuki has been working pretty much on his own for the last 10 years, developing new concepts and techniques by mixing-and-matching elements from different areas of mathematics. The result is that he created his own private mathematical world, so to speak, which no one else seems able (or willing) to venture into for now. So effectively, as it stands his ‘proof’ is not communicable, and thus cannot be surveyed by his peers.

Let us assume for a moment that the ‘proof’ is indeed correct in that every inferential step in the lengthy exposition is indeed necessarily truth-preserving, i.e. no counterexample can be found for any of the steps. In a quasi-metaphysical sense, the ‘proof’ is indeed a proof, which is a success term (a faulty proof is not a proof at all). However, in the sense that in fact matters for mathematicians, Mochizuki’s ‘proof’ is not (yet) a prof because it has not been able to convince the mathematical community of its correctness; for now, it remains impenetrable. To top it up, Mochizuki is a reclusive man who so far has made no efforts to reach out for his peers and explain the basic outline of the argument.

What does this all mean, from a philosophical point of view? Now, as some readers may recall, I am currently working on a dialogical conception of deductive proofs (see here and here). I submit that the dialogical perspective offers a fruitful vantage point to understand what is going on with the ‘Mochizuki affair’, as I will argue in the remainder of the post. (There are also interesting connections with the debate on computer-assisted proofs and the issue of surveyability, and also with Kenny Easwaran’s notion of the ‘transferability’ of mathematical profs, but for reasons of space I will leave them aside.)

Let me review some of the details of this dialogical conception of proofs. On this conception, a proof is understood as a semi-adversarial dialogue between two fictitious characters, proponent and opponent. The dialogue starts when both participants agree to grant certain statements, the premises; proponent then puts forward further statements, which she claims follow necessarily from what opponent has granted so far. Opponent’s job is to make sure that each inferential step indeed follows of necessity, and if it does not, to offer a counterexample to that particular step. The basic idea is that the concept of necessary truth-preservation is best understood in terms of the adversarial component of such dialogues: it is strategically in proponent’s interest to put forward only inferential steps that are

*indefeasible*, i.e. which cannot be defeated by a countermove even from an ideal, omniscient opponent. In this way, a valid deductive proof corresponds to a

*winning strategy*for proponent.

Now, when I started working on these ideas, my main focus was on the adversarial component of the game, and on how opponent would be compelled to grant proponent’s statements by the force of necessary truth-preservation. But as I started to present this material to numerous audiences, it became increasingly clear to me that adversariality was not the whole story. For starters, from a purely strategic, adversarial point of view, the best strategy for proponent would be to go directly from premises to the final conclusion of the proof; opponent would not be able to offer a counterexample and thus would be defeated. In other words, proponent has much to gain from large, obscure (but truth-preserving) inferential leaps. But this is simply not how mathematical proofs work; besides the requirement of necessary truth-preservation, proponent is also expected to put forward

*individually perspicuous*inferential steps. Opponent would not only not be able to offer counterexamples, but he would also become

*persuaded*of the cogency of the proof; the proof would thus have fulfilled an explanatory function. Opponent would thus be able to see not only

*that*the conclusion follows from the premises, but also

*why*the conclusion follows from the premises. To capture this general idea, in addition to the move of offering a counterexample, opponent also has available to him an inquisitive move: ‘why does this follow?’ It is a request for proponent to be more perspicuous in her argumentation.

This is why I now qualify the dialogue between proponent and opponent as

*semi*-adversarial: besides adversariality, there is also a strong component of

*cooperation*between proponent and opponent. They must of course agree on the premises and on the basic rules of the game, but more importantly, proponent’s goal is not only to force opponent to grant the conclusion by whatever means, but also to

*show*to opponent why the conclusion follows from the premises. Thus understood, a proof has a crucial

*didactic*component.

One way to conceptualize this interplay between adversariality and cooperation from a historical point of view is to view the emergence of the deductive method with Aristotle in the two

*Analytics*as a somewhat strange marriage between the adversarial model of dialogical interaction of the Sophists – dialectic – with the didactic, Socratic method of helping interlocutors to find the truth by themselves by means of questions (as illustrated in Platos’s dialogues). This historical hypothesis requires further scrutiny, and is currently one of the topics of investigation of my Roots of Deduction project, in cooperation with the other members of the project.

Going back to Mochizuki, it is now easy to see why he is not being a good player in the game of deduction. He is not fulfilling his task as proponent to make his proof accessible and compelling to the numerous ‘opponents’ of the mathematical community; in other words, he is failing miserably on the cooperative dimension. As a result, no one is able or willing to play the game of deduction

*against*and

*with*him, i.e. to be his opponent. Now, a crucial feature of a mathematical proof is that it takes (at least) two to tango: a proponent must find an opponent willing to survey the purported proof so that it counts as a proof. (Naturally, this is not an infallible process: there are many cases in the history of mathematics of purported ‘proofs’ which had been surveyed and approved by members of the community, but which were later found to contain mistakes.)

Mochizuki’s tango is for now impossible to dance to/with, and as long as no one is willing to be his opponent, his ‘proof’ is properly speaking not a proof. It is to be hoped that this situation will change at some point, given the importance of the ABC conjecture for number theory. However, this will only happen if Mochizuki becomes a more cooperative proponent, or else if enough opponents are found who are willing and able to engage in this dialogue with him.

Well, Mochizuki posted several new 2013-04 items, and at least 1 2013-05 item concerning the framework/methods/tools he used at http://www.kurims.kyoto-u.ac.jp/~motizuki/papers-english.html

ReplyDelete.

So I'd say he's not exactly uncooperative on this. He just seems not to be into direct point to point communication right now.

No idea whether his degree of cooperation will be sufficient for his colleagues.

Yes, I don't mean to say something about M's psychological state or anything, but rather that whatever effort he has been making to make his results intelligible, it hasn't been enough (judging from the piece that gave rise to this post.)

DeleteI'm not sure if I agree that the dialog model captures the problems associated with verifying a proof. These days, proofs are very long and complicated. A classic example is the classification theorem for finite simple groups.

ReplyDeleteAs Wikipedia point out: "The proof of the theorem consists of tens of thousands of pages in several hundred journal articles written by about 100 authors, published mostly between 1955 and 2004."

http://en.wikipedia.org/wiki/Classification_of_finite_simple_groups

There is simply too much work for one human to ever verify in a lifetime. I don't believe the adversary model captures the problem of a proof being so large that the verification is more work that one human can do. I believe this is a fruitful data point for any theory of the sociology of proof acceptance.

Anonymous:

ReplyDeleteThanks, for a neophyte like me that's real food for thought.

But I would take Catarina's (if I may) point to apply in your case: what justifies confidence in the transitive nature of the supposed proof-effect of all these collective efforts?

FWIW: I am really, really out of my element here. I feel like a child at the big people's table.

Yes, that's exactly the point: the fact that very long proofs cannot be surveyed by a single individual does not count against the dialogical account, in fact in a sense it counts *in favor* of it because it emphasizes the social, collective nature of mathematics. Theorems are proved, and then other theorems rely on the original ones having been proved to use them as 'shortcuts' (otherwise everything would have to be proved from stretch). But every bit of it has been surveyed by a 'certified opponent' at one point or another and has been recognized as a valid argument.

DeleteIs it a consequence of the dialogic account that a particular syntactic object might become a proof by way of its writer (or someone) engaging in the dialogic game? so what Mochizuki has provided so far isn't a proof, but it might become one later?

ReplyDeleteI don't have anything at stake here, but my intuitions are partly formed by a proof-theoretic definition of proof that we would offer in beginning logic (a sequence of steps licensed by the proof rules, for example).

Yes, that is one way to cash out the general idea. The main point is that a proof is not a proof unless it is recognized as such by the mathematical community. The underlying idea is a functionalist one. What is the function of a proof? Primarily, to persuade a putative audience that the conclusion follows from the premises. If this function has not been (yet) fulfilled, then perhaps one could say that the piece of discourse in question is 'potentially' a proof, but that this potentiality has not yet been actualized, or something like that.

DeleteMaybe he did claim prematuely. This is what Andrew Wiles did. Human beings are imperfect. If we go on like this, we mathematicians will check and balance ourselves with extinction. If you wish for completely correct all the time, this happens in Heaven only. Mathematics is a field of imagination. But it is also very unforgiving, too much so. If businesmen and politicians were held up to 1/10 of us, we will all have livable future and we will be happy actually.

ReplyDeleteI agree, mathematics is unforgiving, in fact it's the very core of it: it has a built-in uncharitable opponent! :)

DeleteHi Cat, I think I completely disagree with this whole philosophy. Whose idea is it? This is what Thurston said in the Bull AMS years ago. Find and read it. Whole of the mathematics community hated it so much. I think that this philosophical idea is not correct. I will be uncharitable to this idea. This idea can be very abusive in two accounts: It can lower the standard or raise the standard of proofs abitrarily by society. The proofs cannot be juried. Second, there is no foundation of mathematics that is completely true beyond all doubt. Unjustifiable mathematical truth does exists. The nonexistence of proof does not mean it is not true.

DeleteAlso, I want to mention that there are huge amount of literature written by mathematicians who are dead now that are half rigorous but correct. Thurston now fits into this category now. But I just want to mention that the logical correctness cannot sometimes be accessed for quite a while because humans are limited. I do think that we should have a computer checking system for proofs by investing tens of billions of dollars. (That is, computers do not seek proof but merely verifies one given by a mathematician in formal language. Seeking proof part comes into many issues in Logic and so cannot be done. The reverse verification part is doable. After this is done, we mathematicians can act like CS program building to build theorems. Maybe in late 21st century, we will see this?)

ReplyDeleteHi Cat!

ReplyDeleteI've just found this blog today. It' super good, really interesting.

Now - a question - what if there's no opponent? do we cease to have mathematics? do we cease to have proofs?

What about the opposite situation - infinitely many opponents. Does the proponent need to convince/guide all of them? If not, which subset of the opponent set "really matters"?

I believe this sounds more like sociology...

Cheers,

Manny

Hi, I think that actually Mochizuki is a good player. The combination of the importance of the abc conjecture and his position as recognized mathematician makes that other players follow his rules. Also i like the social dimension of the dialogical conception of deductive proofs proposed by Catarina but i share the doubts of Manu if this leads you to reduce poofs to a social activity only. (Sorry for my english if i make grammar mistakes!)

ReplyDeleteAnyone interested in how the story of Mochizuki's claimed proof plays out may enjoy Lieven LeBruyn's "MinuteMochiuzuki" posts, which can be found on Google+. He started by saying:

ReplyDeleteStarting head-on with the 4 papers on inter-universal Teichmuller theory (IUTeich for the fans) is probably not the smartest move to enter Mochizuki-territory.

If you glanced through any of these papers or one of his numerous talks, you'll know he makes a point of 'extending' or even 'partially dismantling' scheme theory using the new notion of Frobenioids, which should be some generalisation of Galois categories.

So if you ever feel like wasting some months trying to figure out what his claimed proof of the ABC-conjecture is all about, a more advisable route might be to start with his two papers on 'the geometry of Frobenioids'.

Lots of people must have tried that entrance before, and some even started a blog to record their progress as did the person (or persons) behind

MochizukiDenial. Here's the idea:"Mochizuki deniers by contrast believe that the claim is not serious. They believe that the body of Mochizuki’s work contains neither a proof outline nor ideas powerful enough to resolve the ABC conjecture. We might be wrong. How do we propose to determine whether or not we are. In contrast to Mochizuki boosters on the internet, we will do this by determining what it is that Mochizuki’s papers purport to do. Stay tuned."

Unfortunately, the project was given up after 2 days and three posts...

Today i tried to acquaint myself with the 126 pages of Frobenioids1 and have a splitting headache because i miss an extra 2Gb RAM to remember the 173 (or more) new concepts he introduces.

However, he seems to be making interesting progress in understanding and explaining some of Mochizuki's machinery.

Thanks for the pointer, John!

DeleteMochizukis paper sounds rather like Grothendiecks 'pursuing stacks' which from what I gather took *some* time before it proved its worth. Heres hoping it makes the same impact even if its looking fiercely impenetrable now...

ReplyDeleteI wonder if anybody is making a concerted effort to model IUTeich & frobenoids in a modern computer algebra system, as the groundwork for testing elements of the proof in a more automated way. That's certainly what I do when trying to understand something in mathematics: I implement a model of it, and if the model works exactly the same way as the theorem, I probably understand it correctly.

ReplyDeleteIt turns out if I take (((10e) (pi - 1) *X) / 2) this produces some differences in sequence near the decimal point, but if I then * (e / pi) the result is an interesting number:

ReplyDelete25.18523247...

As it turns out, the first two digits are 5 * 5, which I call an irrational factorization of 1 * 10. The second two digits are equal to 2 * 9, the fifth and sixth digits are a straight irrational factorization, the seventh and eight digits are 3 * 8. Get this, the ninth and tenth digits are 4 * 7.

It would be interesting to get feedback on whether I have found a way to generally exploit the decimal system or predict decimals of pi, since at no point did I divide e out of the system, and I suspect pi is still present as a factor of some kind.

Catarina, initially you write that the proponent has much to gain from skipping steps in inference, but then go on to reject that this is mathematical practice. I tend to agree with your original statement, actually. For example, although mathematicians sought to elaborate on Perelman's proof of Thurston's geometricization conjecture, still Perelman is considered by the mathematics community to have proved this conjecture, as evidenced by the offering of prizes to him. This supports the dialogical viewpoint of proof as adversial, in that the proponent wins so long as no opponent can provide a counterexample.

ReplyDeleteAs for the extent to which a proof is accepted by the community, it depends on the volume and intensity of opposition. If many mathematicians spend a lot of effort and are unable to find a counterexample to this proof, then the proof in question gains greater acceptance. Framing the debate on Mochizuki's write up, it becomes less of a question whether it is a proof per se, but rather about the degree that the community accepts it as a proof. The question for the philosophy of mathematical practice then is: what inclines or impedes the mathematics community to oppose a proposed proof?