Vdash is a new proposal for a formalized mathematics Wiki, by Cameron Freer . The slides on the Vdash site present a screenshot with an Isabelle/HOL proof, but from the mailing list one can find out that the Wiki is going to be based on Isabelle/ZF. The slides mention a possibility of importing formalized proofs from IsarMathLib as part of the initial library. Cameron’s ideas are perfectly aligned with what I think such Wiki should look like. Needless to say I will be a happy contributor when Vdash becomes a reality.

### Like this:

Like Loading...

*Related*

Tags: formalized mathematics, formalized mathematics wiki, Isabelle/ZF

This entry was posted on September 18, 2008 at 12:57 am and is filed under news. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

September 22, 2008 at 1:32 am |

Does IML use the law of the excluded middle extensively? Without the LEM, proof by contradiction isn’t valid, right? I might be able to convince myself to trust proof by induction (even the constructivists use that), but proof by contradiction seems to require a little more faith than that.

In IML if I’m unsure how one of the tactics brings you from one step to the next, how would I go about getting more detail?

September 22, 2008 at 3:52 am |

really cool. to me there are absolutely no doubt that this is the way to go.

Having a flexible and user friendly tool to publish formalized theorem has the potential to have a big impact in math learning.

September 22, 2008 at 10:01 pm |

pdf23ds,

Yes, Isabelle/ZF implements classical first order logic with LEM. I try to avoid LEM and proofs by contradiction in IsarMathLib whenever practical as I consider it bad style, but still, quite a lot of proofs use LEM.

> how would I go about getting more detail?

I am afraid there is no way to do it other than thinking longer why the step is correct and possibly asking the author. I usually write more detailed proofs and then I try to push the “simp” (or “auto”) tactic as much as possible to shorten the proof. I think even after I do that IsarMathLib proofs are too detailed for most readers.

I agree that it would be nice to have more flexibility in seeing the detail, but Isabelle does not have easy support for that. I heard there is some way of tracing in ProofGeneral what the tactics are doing, but I have never used this.

I believe an ideal system would be something like Metamath with a prover support and a high-level Isar-like language on top of that. The prover would search for proofs of steps of the high-level language expressed in the low level language, kind of like Java compiles to byte-code. This would not only allow the coarse-grained hiding of details with subproofs (like Isar allows with proof … qed), but also examining the finest possible detail like Metamath does.

September 22, 2008 at 11:44 pm |

slawekk,

The proof system I’m working on is geared toward specifically that–making sure all the steps are visible and understandable. I think in the end it’s a tradeoff between ease of use and amount of information available in the proof. Isabelle could probably be modified to support better introspection into the actions of tactics, but given that they’re done by a computer they probably wouldn’t be very readable. Of course, that depends on what lemmas the tactic has available to use. So really what I think would be best is to support editing of a proof after its completion, to make it more elegant. Ideally at some point this could be done wiki-style, because it really is a lot of work for one or a few people.

The main problem in making a new proof system, after making it sound, is to write theory for it. So importing Isabelle theory would be great. Unfortunately, I’m not sure how to map unification to low-level formal derivations (i.e. application of an inference rule to a wff). Probably I would have to implement unification myself or modify Isabelle to export detailed trace information about its operations during proof checking.

I’m still working on the meta language, and I wonder how far I need to go (i.e. currently there’s no built-in typing).

September 23, 2008 at 1:57 am |

Actually, you know what? I think I’m going to scratch trying to build my own formal system, and just copy the metamath system. (That’ll make me feel better about soundness, too.) I looked it up after your mentioning it just now and it looks like exactly what I need. I just need to build a very powerful interface around it to hide all that detail that you don’t usually need. Probably implement tactics and such, but tactics whose operations are transparent.

Can things like beta-reduction be represented in metamath?

You know, I don’t know what’s different about me (and other people into computer proofs) that makes me intuitively find statements like

(from the Metamath book p. 14) to be intuitively ridiculous. Maybe it’s having practically grown up with computer programming? For some reason, my intuitions are just different, you know?

September 23, 2008 at 10:53 pm |

I think you are making a right decision here. Metamath is rock solid and it is there already.

This is probably correct if we talk about proofs written and verified by humans.

What Whitehead and Russel did in Principia was like trying to build concrete buildings by gluing grains of sand together, one by one. The result does not prove that the idea of building from concrete is a failure, only that you need the right tools to do that.

As for the length of the formalizations you may be underestimating the effort needed to create libraries of formalized mathematics.

There is an interesting note by Freek Wiedijk on estimating the effort required. I personally don’t worry about it. To me doing formalized mathematics is fun, why should I worry that the supply of that fun is limitless?

To be honest, I don’t even know what beta reduction is. The Asteroid Meta site used to be a kind of forum for Metamath, you may want to ask there. There is also a Metamath Google Group.

October 6, 2008 at 5:46 pm |

Can things like beta-reduction be represented in metamath?

Probably. Curry and Feys managed it in Combinaroty Logic, but I fear you’d end up with a theory of substitution, captured variables, and so forth, and have to formalize that. Either that or devise a set of variable-identity constraints like the ones they use in metamath. Metamath doesn’t automatically rename variables on substitution — you’d have to do all that explicitly.