12 Dec 2002 moshez   » (Master)

raph: May I ask what the point of all these computer-verified proof systems? I mean, yes, we all proved in Logic 101 that it is theoretically possible, but seriously, what's the point?

Let me first clarify some things.

Mathematicians do have mistakes in their proofs, many times. However, I seriously doubt such a system will actually help solving that problem. I can speak with some authority, having a little experience in writing papers, that writing a complete proof of a non-trivial statement would quickly become onerous, and more bugs would be made in the translation.

I have learned, and taught, advanced math. Teaching math is about giving intuition through proofs. Proofs written up as formal list of statements give no intuition, nor an idea of how to solve similar problems, which is what teaching mathematics is all about.

It is a nice toy. It is even fun to enter a few simple proofs. But, having done some formal proofs, my experience is that the novelty wears off and it becomes a mechanical boring process (and I like this stuff, basically!).

So, I think I've discounted "helping mathematicians", "improving math teaching" and "having fun" as possible motivations. Either my logic is wrong (pun not intended) or I have not listed all possible motivations: which is it?


Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!