In an interesting interview in the most recent issue of the ever-interesting electronic journal The Reasoner, Mateja Jamnik of the University of Cambridge argues that it might be possible to automate the invention of the kinds of visual images, or representations, that mathematicians sometimes or often use to get insights into the development of mathematical proofs. Her argument is significant in part because, if successful, her argument undercuts one of Roger Penrose's arguments against purely computational theories of the mind (or brain). Beyond that Jamnik's argument raises the ever-interesting question of why visual models (sometimes considered "informal") are as important as they seem to be in "exact sciences" such as mathematics and physics.
Here are some snippets from this fascinating interview:
Mateja Jamnik: I think that a proof is a social construct in mathematics. I think the history of mathematics shows us that where mathematicians—famous mathematicians—came up with a solution or a proof of a problem or a theorem,and presented it to other famous mathematicians,as long as they convinced them, they trusted that that was the correct proof. Andit was only when the logicians came along that they formalised the logic of that domain and were able to either prove or disprove the proof, to actually formalise it. And that’s what we mean when we talk about the formal proof, that you can verify that it is correct, that it follows from a set of axioms and so on. Whereas mathematicians, I don’t think, are very interested in that.They are really more interested in the insight in the proof, and trying to understand why the theorem holds, and that’s why I say it’s a social construct because as long as they convince enough people that it’s correct, nobody’s going to go and check it out to see whether it is or not. I mean, as long as fellow mathematicians believe that they understand and that they trust the process of the proof, then they’re fine. And history of mathematics is full of examples like that, where there are proofs that were thought to be proofs for fifty years and even by very famous people, and they were disproved and it was shown that they were not proofs at all. Whereas, from a formalist point of view, formal proof has a very technical meaning, which is that it follows from a set of axioms.
[snip, snip]
ML [interviewer Mary Leng]: So what interests me in your work is that you’re saying that these methods, though visual,can be formalized.
MJ: Yes, that’s exactly what I’m trying to do.
ML: Whereas some of the thought in thinking about diagrammatic reasoning in philosophy is to say that there’s this element of our cognition of mathematics that isn’t formalizable. I suppose that’s something that Penrose is pushing at as well, in his claim that there are diagrammatic proofs that cannot be automated, because he wants to push the idea that there’s something special about us, that we’re not purely computational.
MJ: That’s right. It is. But what I’m trying to show is that all these so-called ‘informal’ methods, they can be formalized. And so I’m looking into the use of diagrams. In fact I just came from a conference on diagrams where everybody was coming from areas of mathematics, philosophy, cognitive science, cognitive psychology, computer science, artificial intelligence,and basically we have a common interest, which is to study diagrams, and the applications and theoretical foundations of the use of diagrams. And there are lots of people who come up with representations—diagrammatic representations—that they formalize and they use reasoning on. So it’s totally possible. And also my work for my PhD, on DIAMOND [Jamnik’s interactive theorem prover, which made use of diagrams to construct proofs of theorems], was in the domain of natural number arithmetic, where the proofs were not at all like the normal logical proofs. In fact, I would say that one of the hypotheses that came out of that work was that people use something like what we call ‘schematic proof’ to find a solution to a problem. So basically, you look at a few examples—concrete examples—of your problem and you solve them, and then you spot the pattern and you generalize that pattern, and you try to make an argument about how that pattern is a justification for the general statement for all cases. So what I did with natural number arithmetic was that I would represent these theorems and statements in mathematics using diagrams, and then use just manipulations of concrete cases of diagrams—for some natural number like 5, 6, or whatever—and then spot the pattern and generalize this into a program which, basically upon input, will produce a solution for that particular case. We call this—this program, this general pattern, this procedure—we call this ‘schematic proof’. My hypothesis is that this is one possible model of how people do proofs, and there’s plenty of evidence of that from history.
[snip, snip]
ML [interviewer Mary Leng]: This brings me to the issue about Penrose, because Penrose wants to say that we’re fundamentally different from machines. You mention in your book (Mathematical Reasoning with Diagrams, 2001) Penrose’s scepticism about the possibility of modelling diagrammatic reasoning in computers, and I suppose behind all that is the thought that we want to find things that we can do that computers can’t. So if it turns out that we can model this reasoning in automated settings, then that speaks against this idea that we’re so different.
MJ: Yes absolutely. I think that we don’t understand reasoning enough to be able to make claims like this. So what spurred me on to say something about Penrose in my book is because he presented this example about a cube—about something which is innately human reasoning that machines wouldn’t be able to do. He presented this example of a proof that the sum of the first n hexagonal numbers is n-cubed. He presented this visual proof which basically says, “I’ll give you an example for a cube, that is of size three, and if you split it up in this way you can see that those are the first three hexagonal numbers, and if you continue doing that, then you understand that the general theorem holds.” And that’s precisely what, for example, the theorem about the odd natural numbers, in 2-D, is. It’s an analogue of that in 2-D. And I thought, there’s something very procedural about this. You know, and we see, I suppose he’s appealing to the fact, the visual effect, that you sort of ‘splatter’ the 3-D onto 2-D to see that those three shells of the cube form a hexagonal number. But you can think of it in the same way about the odd natural numbers. You have that the sum of the first n odd natural numbers is n-squared. You can take a square of size three and then you split it into ‘ells’, and you see that each ell is the subsequent odd natural number. And that’s exactly an analogue of what Penrose presented. And obviously I showed we can capture that, you know? DIAMOND could easily do that. OK it doesn’t have a 3-D interface, so technically you can’t, but in principle, there’s nothing that would stop it really. So I suspect that Penrose is asking, really, “Could the computer come up with an idea like that?” and we don’t know that yet.
ML: So just to clarify, DIAMOND is a proof checker rather than a theorem prover?
MJ: It’s an interactive theorem prover, so it means that the user constructs the sample cases, so it means the user has the insight, really, into what the proof should look like. So the computer’s not coming up with an insight.
ML: In your book you mention the hope that you could actually develop a computer program that could do the insight steps. How have things moved in that regard?
MJ: I haven’t moved much in that direction yet, because I’ve been looking at a different direction with reasoning with diagrams, but that would definitely be the next step, to put some sort of search procedure on top of all these visual methods and geometric manipulations of diagrams and check whether anything interesting comes up. Now of course Penrose would probably say, the computer doesn’t have the insight. But where does that come from in a mathematician? It comes from experience, it comes from...well we don’t know. That’s why I’m interested in modelling this type of reasoning.
&&&
The dynamic evidence page
Evidence marshaling software MarshalPlan
