So there’s a piece in Vice which quotes me as saying that I fear “all published maths is wrong”. Of course this is nonsense: indeed, as every mathematician knows, some published maths is wrong, but the vast majority of it is fine (indeed some of it has even been checked in Lean 🙂 ). The idea of how much of the literature is wrong/incomplete/whatever came up in the context of explaining various viewpoints which Patrick Massot, Michael Harris and myself had been exploring during our PhilMath Intersem last June, but for the record, “all published maths is wrong” is not something I fear, because I know it’s not true. There is another quote attributed to me: “I think there is a non-zero chance that some of our great castles are built on sand”, which I did say, and which I think is a far more accurate representation of my views (but rather less clickbaity). I guess that this viewpoint — that maybe some important stuff is not ok — is not believed by all mathematicians. Some seem to think that all the important stuff is fine, and I’m less sure.
But I also spoke about Fermat’s Last Theorem in the article, and made a claim which again not everyone in my community seems to believe — indeed Persiflage expressed an opposing view on Twitter. The claim I made is that no human knows a complete proof of Fermat’s Last Theorem. Speaking as someone who was doing a PhD in precisely the area used by Wiles and Taylor at the time it all blew up, I am lucky enough to have an overview of the argument — and certainly Persiflage does too. But does one human know all the proof? Last year I asked Wiles if he knew all the details of his own proof (30 minutes in), and he does not say “yes”. Indeed he says that he would not want to sit an exam on the proof of Langlands–Tunnell.
So what does it mean to “completely understand a proof of Fermat’s Last Theorem”? Vice quotes me as saying that nobody “completely understands” it, but it also claims that I suggest “(nobody) knows whether it’s true”, which again is a bit misrepresentative. There are people that I trust, who have checked the parts which I have not checked, so I think we can argue that I know (to the extent that a human can know anything) that FLT is true. But what about finding that one person who “completely understands” it? Let’s take Wiles’ interpretation — could we find someone who is guaranteed to pass an exam whose syllabus was all of the mathematics involved in the proof? I think we should make it an open book exam, so the human being examined can look at the literature — but they cannot consult other humans.
And here I’m going to stick to my guns. To completely understand a proof of FLT (let’s say, for now, the proof explained in the 1995 Darmon-Diamond-Taylor paper) you will need to be a master of the techniques used by Langlands in his proof of cyclic base change (and I know people who are), and a master of Mazur’s work on the Eisenstein ideal (and I know people who are). But what about the far less sexy technical stuff? To move from the complex analytic theory of modular forms to the algebraic theory you will need to know the delicate interplay between the analytic and algebraic theory of moduli spaces of elliptic curves (and I know people who know this — but I went through some of this stuff once and it’s far more delicate than I had imagined, and there are parts of it where the only useful reference seems to be Brian Conrad’s brain). This last example is perhaps a good example of a tedious technical issue which it’s very easy to forget about, because the results are intuitive and the proofs can be technical. There are many other subtleties which one would have to fully understand because they’re on the syllabus. Is there really one human being who would feel confident answering questions on all of this material? I am really not sure at all.
And I think the reason I am not sure is because Lean has taught me that checking the details can sometimes be hard. If someone had asked me two years ago if I knew the definition and basic properties of adic spaces, I would have said “sure — I even wrote a paper about them”. But when formalising them I realised that there were all sorts of subtleties which I had just “taken for granted” because they were tedious technical issues which “of course I could work through in theory”. Actually working through some of them, when formalising them, made me understand that some of these issues were far bigger and more complex than I had realised. In the perfectoid project there is still an issue regarding the topology on an adic space, which I had assumed would be all over within about a page or two of pdf, but whose actual proof goes on for much longer, and at one point even invokes Hochster’s thesis (which I’ve certainly not read), although Conrad assures me that it is not necessary. We’ve formalised the definition, but there are still some very basic properties of adic spaces which we have not formalised. Maths is hard. My belief is that, over time, mathematicians begin to forget this, and they start to conflate the idea of a result being “standard” with the idea of a result that they completely understand the proof of. Our notion of proof is so different to the formal notion that we skip huge steps knowing that the techniques will work, and after a while we may forget what is involved in these techniques (if indeed we ever knew). This observation is not really of mathematical relevance — if I need the Langlands–Tunnell theorem in my work (and I did, once, in my work on Artin) then I will invoke it and not lose any sleep over it. But on the other hand, do I really completely understand the proof of that Artin work — my own theorem? I wouldn’t say I did.
OK, I definitely think “open book” has to be allowed. Let’s think of it as a qualifying exam. But I also think that *any* proof of Fermat will do, you don’t need to use Wiles’ exact argument. So here we go (until my coffee runs out):
Examiner 1 (Xena): OK, so prove Fermat’s Last Theorem:
Candidate (Persiflage): OK, so this is what I want to do. I’ll start with a very broad outline.
Step 0: Take the Frey curve. By Mazur (plus classical cases) you can assume E[p] is absolutely irreducible.
Step 1: Use the Khare-Wintenberger argument to construct a compatible system over Q of 2-dimensional weight [0,1] representations of “conductor N=2”.
Step 2: Use a Fontaine type argument at p=3 to deduce that no such family exists.
Let’s unravel this slightly: I gave a full topics course on Mazur’s paper at Harvard once. I’m not sure any of the students got anything out of it, but I learnt quite a lot. Note that the required theorem for Step 0 does not use everything in the paper. Step 2 is also something I know well.
Examiner 1: Ooh, you have to be careful. Are you going to use Fontaine’s estimates for higher ramification groups here? Can you prove that?
Examiner 2 (TG): Let’s hear him out.
Candidate: I took a course on finite flat group schemes from Schoof that covered this! But let’s get back to the outline. The key point of KW involves estimates for dimensions of (reasonable) deformation rings, but also an R=T theorem over totally real fields in a nice (ordinary or Fontaine-Laffialle) setting where p splits completely.
Examiner 2: How are you showing that E[p] is potentially modular?
Candidate: I’m finding another elliptic curve with A[p]=E[p] and A[q] induced. So I’m using modularity lifting and residual modularity of dihedral representations. So you have to add Hecke and Moret-Bailly to things I need to explain. I might even force A to have (potentially) good reduction everywhere (outside p where it might have multiplicative reduction if it has to) for convenience. Then again, maybe I want to insist that A has multiplicative reduction at at least one place for convenience later on.
Examiner 2: Very good. Continue.
Candidate: So I think the main thing is now an R=T theorem over a totally real field in a context where all the local deformation rings are smooth.
Examiner 1: Hang on, how are you constructing a map from R to T here? I seem to remember that was a bit tricky, and Richard had to write a paper covering the last remaining cases.
Candidate: There’s a lot of flexibility here, I’m sure if I can squeeze in some primes which allow me to pass to a Shimura curve…
Examiner 1: Oh here we go, I think you might be in trouble now — are you saying you can prove Jacquet-Langlands?
Candidate: It’s open book, right? (slight sweat beads forming) Note that something quite a lot less than the full Jacquet-Langlands is required here?
Examiner 2: Remember that he only has to prove that *someone* can prove Fermat completely; it doesn’t have to be him.
Examiner 1: Can you prove the Greenberg-Wiles formula?
Candidate: The best way to screw anyone in an exam is to go back to basic theorems they last thought of 10 years ago. I think I have seen all the details and with an open book…
Examiner 1: What about comparisons between the analytic and algebraic theory of modular forms, there are some subtleties here…
Candidate: OK, I think one has to distinguish between “proving a theorem” and “proving a theorem to the level of detail required to program into a computer” — I don’t think the latter is a fair way to judge what a proof is.
Examiner 1: But that’s my point!
Candidate: But if that’s your point, It could make proving something like the main theorems of class field theory extremely tedious, and surely you wouldn’t claim that nobody knows the proof of CFT?
Examiner 2: Let’s take a break; I think I just saw a generation 4 Pachirisu walk past.
LikeLiked by 2 people
This was kind of my trump card — if you wanted to bypass some stuff with Khare-Wintenberger then I was going to challenge you to prove Jacquet-Langlands, including the non-compact case. But actually I’d forgotten about Greenberg-Wiles! This actually is something which we’re working towards in Lean (or, more precisely, stuff from Milne’s arithmetic duality theorems, which I thought was a really good target for formalisation because a lot of it is pretty formal anyway, and there are sometimes rumours that some arguments in that book are incomplete). To be honest I am unclear about how much analysis is needed in those proofs; in Isabelle they have stuff like Dirichlet L-functions and infinitely many primes in an AP, but we’re missing this stuff in Lean right now. But on the other hand if you have Cassels-Froehlich to hand then maybe it will all be fine. I reckon you still need that trace formula stuff though. Do you know it? I will freely confess that the details of the trace formula in the non-compact case are still a mystery to me — I should work harder.
I guess E will always be semistable at some auxiliary prime q|abc. Carrying this prime around one should be able to guarantee that everything is compact at infinity by taking quaternion algebras ramified at all primes above q. (One may as well, and probably can’t avoid, assuming that [F:Q] is even.) I have some sense how the proof of Jacquet-Langlands goes, but I guess I certainly can’t really claim to “know” it. But in an open book exam I’m not sure it would be impossible… Of course (as you alluded to on twitter) I don’t know really “know” the full details of the construction of Jacobians over Z either. Naturally, I’m the type of mathematician who doesn’t actually “know” very much and operates mostly on instinct. (Imagined conversation in my head: GB to me: do you really know the details of anything? TG: (laughter) GB: no, I’m serious.)
And thinking of co-authors on the 10 author paper who have obviously thought much more about trace formula things before, I would wager that Ana, Peter, Richard, and Jack might be up for your challenge!
I asked Richard this question a long time ago and he also didn’t answer “yes”. Perhaps things have changed since then. Maths is really hard though. My co-author Patrick has just written something in our forthcoming paper, about a lemma in Bourbaki’s commutative algebra which, when he tried to formalise it, took an age simply because the argument they were suggesting seemed to need more input than they had realised. When you start in this game it’s scary what you find. Ultimately he had to think about things a bit more conceptually, and then he found an easier proof.
How about the “theorem” that classifies finite simple groups? That’s a great castle.
Hey Ken! I am particularly concerned about the classification — I am worried that this proof will die. There are 11 volumes planned of which I think we have 9 (or maybe 8?), but everyone is getting older. Whether or not this proof is complete (and it wasn’t complete once, when everyone was saying it was…), one can imagine a future where the volumes don’t get completed, and then in 20 years’ time, even if computers can read and understand well-written human text — what happens then? We have to confess that we lost the proof?
LikeLiked by 3 people
First of all, I think the point of mathematics is exactly that we collectively know something to be true. So the mathematical knowledge should be the union (instead of intersection) of (mathematical) knowledge of mathematicians. To that end, I consider requiring an individual to know all the details of all the mathematics involved in an argument to be absurd.
Secondly, to your fear of we may lose the proof of big theorems. If the statement is correct and provable once in the history, there is no reason that it cannot be reconstructed again in future with all the new insights and all the old papers already available concerning that specific statement. Maybe I’m being too optimistic about that here.
Lastly, how is the fear of “great castles” might be “built on sand” (significantly) differ from being agnostic about the existence of anything…? Instead of asking:”what if some big results turned out to have a gap and be actually untrue”, one might keep asking:”what if all of these mathematics are just my fantasy in a matrix/simulation/13th floor?” Also, if one needs a program to check all the proofs, who’s gonna check that program? Another program-checking program? And a program-checking-program-checking program, etc.?
LikeLiked by 1 person
In an ideal world this approach would be fine. But what about the crank proofs I get in my inbox of the Riemann Hypothesis? Those people “know” they’ve proved it — but that doesn’t mean we should add RH to the list of mathematical knowledge. I agree that *requiring* one individual to know all the details of a proof is nowadays absurd. But my observation is simply that I’m not convinced that such an individual exists, not that I’m demanding that one needs to exist. I don’t trust the cranks who tell me they’ve proved RH. But what has happened to me personally is that I’ve realised that trusting a result which is claimed by an expert and whose proof has been read in detail by a small group of experts is also taking a gamble. A far smaller one, to be sure. However mathematicians proceed as if there were no gamble at all. As maths gets bigger and bigger, those small gambles are adding up. That is what concerns me. In short, I agree with your first paragraph.
The second paragraph — the reality is unfortunately less simple. The original proof of the classification theorem involves results which were never published but which are known to the experts. There is currently a big effort being made by a small number of people (most of whom have now actually retired) to write everything up properly. If they get those volumes finished, that’s great. If they don’t then there’s the issue that some of the tricks might be lost. And unfortunately finite group theory is now no longer the fashionable area it once was, so there are not the new experts there to replace the old ones. Those “new insights” which are of course occurring in lots of places in mathematics — I’m not so sure they’re occurring in finite group theory. This is an issue of genuine concern to me.
As for your final paragraph, I think this is dodging the issue. Of course we can philosophise about what exists etc etc, but there is an issue at stake here. Most of modern pure mathematics is *absolutely pointless* and don’t let anyone try and convince you otherwise. Some of it is super-useful, but a lot of what I did when I was an active researcher is just postulating and proving links between abstract objects. Given that it is pointless, the *only thing it has going for it is that it is true*. If I cannot even be sure that it is true, then it is close to worthless.
As for who is going to check that program etc — this problem has been solved. There are two things to say. Firstly, it is clear that having something of this nature checked by a computer is an order of magnitude more reliable than having it checked by a human. And secondly, three independent type checkers, in three different languages, have been written for Lean which can be used to verify Lean’s certificate that a theorem is valid. To check that Lean has correctly verified a proof, we don’t need to check that Lean has no bugs, we just need to check that it did its job correctly on that one occasion, and this is what the typecheckers can do. This is a technical issue and you’d be better off talking to a computer scientist about this, but they have thought about this extremely carefully. I am quite happy with the first observation — I believe that computers are far far more reliable than humans, and given that we’re stuck in the real world with all its imperfections, I’ll take a computer proof (and I’ve never seen Lean proving something false) over a human proof (and I’ve seen many mistakes in maths papers, some serious) any day. I agree that the “level” for what people regard as an acceptable proof will be different for different people. But for me, mathematics is black and white, and I am sick of reading unclear/ambiguous statements in maths papers. I used to think that if I didn’t understand a line in a maths paper then I was the stupid one. But maybe the author wrote unclearly — or maybe the author was just wrong. I spent 15 minutes this afternoon staring at a claim that the fact that a map was a bijection was “clear”. I still don’t think it’s clear, and my proof which justifies the bijection is long. Now I think that humans are sloppy. With Lean proofs I can just right click and trace everything back — there is an answer to all my questions in a Lean proof.
LikeLiked by 1 person