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.


Tags: , ,

7 Responses to “Vdash”

  1. pdf23ds Says:

    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?

  2. nicolas Says:

    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.

  3. slawekk Says:

    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.

  4. pdf23ds Says:


    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).

  5. pdf23ds Says:

    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

    The Principia Mathematica was the crowning achievement of the
    formalists. It was also the deathblow of the formalist view.. . .
    [Russell] failed, in three enormous volumes, to get beyond the
    elementary facts of arithmetic. He showed what can be done in
    principle and what cannot be done in practice. If the mathematical
    process were really one of strict, logical progression, we would
    still be counting our fingers.. . .
    One theoretician estimates, for instance, that a demonstration
    of one of Ramanujan’s conjectures assuming set theory and elementary
    analysis would take about two thousand pages; the length
    of a deduction from first principles is nearly inconceivable. . . The
    probabilists argue that. . . any very long proof can at best be viewed
    as only probably correct. . .

    (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?

  6. slawekk Says:

    I’m going to scratch trying to build my own formal system, and just copy the metamath system.

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

    The probabilists argue that. . . any very long proof can at best be viewed
    as only probably correct. . .

    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?

    Can things like beta-reduction be represented in metamath?

    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.

  7. Hendrik Boom Says:

    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.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: