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?

Thanks