I won't be at OSCON, but as it turns out I'll be in San Diego from Monday through Saturday next week anyway, for Pacific Yearly Meeting of the Religious Society of Friends (Quakers).

I might be able to get away for a few hours. It would be really fun to meet with friends. I probably won't be in ready phone or email contact there, but get in touch and we'll see if we can set something up.

Proofs

I think that computer-checked proofs are inevitable, but not particularly soon. None of the existing formal proof projects are Web-aware in the sense of fostering distributed collaboration. The big step, I think, will have to be taken by someone who understands the Web deeply, and enough formal logic to get by. I have the feeling that huge technical prowess is not necessary. Making a usable system doesn't have much to do with "corner cases" in logic.

As Bram points out, I think the big technical issue is making proofs robust with respect to choice of details. In existing systems, they seem to be fairly brittle. For example, Metamath uses the standard set-theoretic encoding of numbers. Proofs of theorems in number theory work no matter what encoding you choose, or even if you use an axiom system rather than an encoding. It shouldn't matter which axiom system you use either. In a sense, number theory is in terms of a "Platonic" ideal of numbers.

But you don't see that from looking at the proofs in the Metamath database. There, proofs are in terms of the specific encoding. Trying to adapt these proofs to a different encoding would probably be difficult, and would more likely than not involve digging into the proof itself.

For example, this is a theorem in the standard set-theoretic encoding of naturals: forall x and y, x > y <=> x = x \union y. However, in other encodings it will be false, and in others it will have no meaning. Somehow, you have to show that the proof is respecting the abstraction, not piercing it and accessing the encoding. Metamath, while brilliant in many other respects, doesn't seem to have an easy way of doing this.

In logic, "any theorem over naturals in one encoding is also a theorem in any other encoding" is known as a meta-theorem. Ordinarily, you can apply a theorem using plain old substitution (and, usually, some constraints that variables are disjoint). However, the rules for meta-theorems are hairier.

I'm convinced, though, that the understanding of the Web must run deep, or the project has little hope. In fact, there seem to be two fairly large-scale projects to formalize math in a machine-checkable form, both initiated by mathematicians, and neither with a high profile today. One, Mizar has nonfree software, and uses the structure of a refereed journal. Another, QED, doesn't look like it's been updated in a while. I haven't seen anyone even try to adapt a proof done in one system into another.

I should also mention NuPrl, which is GPL. The focus is a bit more on automated theorem proving, although they do seem to have nice library of proofs. Also, NuPrl is based on constructive logic.