[QUOTE=Dominic Mulligan]
Where do you stand on the role of computer assisted proofs in mathematics? Proofs involving gigabytes of data only checkable by automated means - proven or not?
How much do you read outside of your area? For example, there seems to be a movement within computer science to define formal denotational semantics of programming languages via category theory and other forms of abstract mathematics. Do you read around the mathematical sciences to see whether you’re research may be applicable there, or does this not concern you?
Which of the remaining Millennium Problems do you anticipate to be solved first?
[/QUOTE]
For your first and last questions, I imagine if you asked X many mathematicians, you’d get X many answers. (Well, with X not greater than 6…)
My own views are that it’s distressing how few mathematicians have familiarity with computer proof systems, and that, ideally, all proofs should be routinely formalized, typed up, and verified. Unfortunately, such systems as exist today are far from practical enough for this to be so routine; they involve too much tedious boilerplate and low-level shuffling in the formalizing of most real mathematical proofs. Still, that is the goal which we should be striving towards.
Of course, what you’re really getting at is the business of the proof of the four-color conjecture, and similar things. The controversy over that proof basically breaks down into two parts: first, we should we trust the results of the computer program involved, when there could have been a bug in the program, the compiler, the hardware, etc.? All this is true (bugs are a fact of life), but not really specific to computers: human-written mathematical proofs are just as likely to contain bugs, human computations can suffer glitches (who hasn’t experienced a situation in which they keep making the same arithmetic error repeatedly?), etc. So if you’re looking for 100% reliability, you’re not going to get this from computers, but you’re not going to get it from humans either; it’s too lofty and unrealistic a notion of what proofs really do. Numerous are the times that a proof has been considered valid by mathematicians, only to have been discovered to be flawed much later. The best you can get, as far as proof goes, and this holds for math or anything else, is something in a form that can be subjected to repeated scrutiny, looking evermore for the bugs, and eventually feeling confident enough that there aren’t any. And this works as well, or really better, with computer-formalized proofs than with human proofs. If you’re worried about compiler bugs or hardware bugs, you can keep writing new compilers and testing it out on new hardware. If you’re worried about bugs in the actual program of the proof itself, that actual program will be something human-written, and just as manageable and amenable to human inspection as any other sort of proof a human can come up with.
The second part of the controversy with the four-color theorem is the business of the brute-force computation being so “large” as that no human could ever hope to step-by-step verify it. Again, though, this isn’t really a problem specific to computers; a proof created in many parts by many human mathematicians, like the classification of the finite simple groups, will suffer similarly. It’s always desirable to bring a lengthy and wild proof down to size and make it more manageable, both in terms of increasing our trust in its lack of errors and in terms of gaining something which can more readily impart “understanding”, but it doesn’t mean we have to reject entirely the wild proofs.
Perhaps the problem is with the binary view of proof acceptability. A proof either is valid or it isn’t. Well, certainly, with a fully formalized argument, in a Platonic sense, this is true, but it is a notion rather detached from the way mathematics is really done: almost no real mathematical proofs of any length are so fully formalized (though, as I said, I would like to see a greater degree of formalization and mechanical verification), and, both of those that are and those that aren’t, any process of proofchecking available to us will always be fallible. There’s just no way around that. So rather than a binary view of proof acceptability, we can grade proofs by how much trust we put in the assumption that they are bug-free: some proofs are very clearly buggy, some proofs are small and graspable and viewed as almost certainly bug-free, and then various other more hirsute proofs lie somewhere on the continuum of reliability (“Oh, I’m pretty sure that their argument was legitimate, though I wouldn’t bet my house on it”).
So… those are my views. Obviously, others will feel (very) differently.
I’m personally very concerned with connections between abstract research in logic and various potential applications in the denotational semantics of programming languages, but you’ve just happened to get lucky with where my interests lie. I think most mathematicians do read around a bit, into areas somewhat adjacent to theirs, not necessarily only to see if their work has applications, but also just out of pure intellectual interest in matters similar to those which they’ve found interesting enough to work on.
I have no idea which of the remaining Millenium Problems will go down first; the one I have the most familiarity with is P ?= NP (often called the greatest open problem in logic, and thus the one of most concern to me), and the one that’s been around the longest with the most attention paid to it is the Riemann Hypothesis (often called the greatest open problem in all of mathematics), but I’m really not aware of any rumblings anywhere that are on clear paths to blowing up into solutions to any of them. (That is why they’re open problems of such note, I suppose. No one has any real idea of how to go about proving/disproving any of them, so any work towards doing so is expected to involve seminal developments of new and productive constructs.). I’m kinda hoping the Goldbach Conjecture (which was, incidentally, bundled with the Riemann Hypothesis by Hilbert) gets solved soon, personally, though I think there’s even less rumblings of progress on that problem than on any of the Millenium Problems. It’s just been around so long, though, and now that Fermat’s Last Theorem is down, its time has come.
Well, that and the connected but much much older twin prime conjecture, which has been open for some embarrassing 2300 years.
…