It's great to see how much interest and excitement vdash has
generated. Thanks for getting in touch!
The site hasn't launched yet (though as Null Set points out, there's
a MediaWiki installation which I've been modifying slowly). I'll
write up a longer document with the proposed structure shortly. For
now, here's a brief outline of the minimal steps necessary to get a
prototype up and running.
1. Isabelle interface that asynchronously verifies entries and makes
appropriate notes in the SQL database. In particular, links to
definitions or results on other vdash pages should be processed as
2. MediaWiki parser of Isabelle/Isar proofs (possibly via GeSHi)
which also displays data about verification.
3. One-time conversion of IsarMathLib to seed the wiki.
4. Finalize license issues. I now believe there are good reasons
for content to be in the public domain (rather than under the BSD
license, as noted in the e-club slides) but with a strong informal
culture of attribution. I'll elaborate on this issue shortly.
Other features that would be nice in the relatively near future:
4. Method of locking-down verified pages. Perhaps allow only edits
of verified pages that are themselves correct, or allow only forks.
5. More sophisticated versioning of proofs. When a page changes,
allow for links that automatically point to the new statement, as
well as static links to the old version.
6. Parse error messages from Isabelle in a useful way.
For example, a script might take subgoals noted in Isabelle error
messages and expand the document with the outline:
show ___ fix ___ assume ___ sorry
7. Display attribution in a detailed manner, sorted by degree of
8. Automated feeds/scrapes from open-access sources (with
appropriate licenses) to create stubs as targets for formalization.
There are many other interesting directions for both UI and back-end
enhancements. I'll soon post some more of my ideas, as well as
pointers to existing tools and proposed features. But I'd also love
to hear what technical ideas you all have, in what ways you'd like
to contribute, and in what directions you'd like to see this go in
> Is individual statements going to save in some separate database?
> Mediawiki's revisions isn't the best format to store data because
> converting around would be difficult.
> I also find categorize items in mediawiki a huge pain.
> Other than mediawiki is the most popular wiki system out there, I
> don't see too much advantages for this.
> Chao Xu
I agree that MediaWiki may not be the best choice. In addition to
being very popular, it is also fairly mature and has many
extensions, but in the long run we may be better off using something
else, or building our own wiki.
SWiM, which Ian (drevicko) has mentioned, is based on IkeWiki.
I suspect that using IkeWiki at this stage would add a lot of
overhead (for semantic metadata) without corresponding benefit.
My inclination had been to modify MediaWiki for now, and maybe
eventually migrate to a custom-built system, but I'd appreciate
hearing other suggestions people may have.
I love MediaWiki and administer numerous instances of it for varied
purposes. Nonetheless, I wonder how easy it is going to be to plumb
its content database to semantically meaningful proof libraries. It
seems to me like the ultimate Web 2.0 challenge.
However, it probably won't be any harder than any other wiki framework,
and MediaWiki can be made to take care of so many formatting and
organizational issues automagically, and it a fast way to get
collaboratively generated content online.
But surely the wiki just acts as a gui for a revolutionary backend
mathematical knowledge database. There have been so many partially
successful demonstration projects before (QED Project, etc) that
withered mainly, IMHO, because they were too specialized, and couldn't
easily be enough things to enough people.
What's deeply meaningful about math is not mathematical facts
(theorems) themselves, but the highly intricate graph of inferential
connections between them. These connections need to be be tracked in
three different ways.
1) hard core logical connections (MetaMath is a good example of this, but
its proofs aren't very human friendly, and its subject scope is limited)
2) intermediate technical (the kind of proof presentation lines that
working mathematicians like to see in LaTeX) and
3) pedegogical -- the ability to backtrack from one mathematical statement
to more elementary ones, perhaps with well placed explanatory notes
available in the presentation).
I've long felt that any ultimately successful mathematical knowledge
base would have to map all three kinds of connections onto a single
collection of theorems -- without ever internally confusing apples and
oranges -- which won't be easy.
It will also be interesting to see how the system keeps track of what
axioms every single statement assumes or doesn't assume. E.g. some
part of proven math theorem space needs the Axiom of Choice invoked
somewhere in its proof tree, and some part can do without it.
Modular ("object oriented") design will be key here, so that different
front ends and various proof checkers can interact with the same
foundational database. Importing mathematical knowledge into this
database without confusing shades of meaning between different fields,
schools of thought, and individual mathematicians, will be quite a
semantic challenge. But, if successful, this could place mathematics
on a firmer logical foundation than it has ever been before. Someday,
no new proof will be published before it is first digested by a
checker (or several) against a comprehensive mathematical knowledge
base to see if it provokes contradictions with anything else we think
we know. There is no such thing as an isolated mathematical fact.
I'm in awe at the goals and motivations of this project and I dearly
hope it succeeds. But that will require both design brilliance and
bountiful amounts of highly skilled help to import a large amount of
mathematical knowledge from its currently distributed, disparate and
overlappingly repetitive forms. It's quite a bit of informational
entropy that needs be reduced so we can have it all in an essential
form with interfaces that make it useful to many.
I agree on all points. Ultimately, we may move to a custom wiki
engine, and all manner of elaborate in-browser editors, but we can
get quite far without either of these yet.
Your proposed ban of consistency-destroying activities, and easy
snapshot-downloads seem like great places to start.
There are also many useful (but not especially flashy) UI
improvements that we can make (like parsing of Isabelle error
messages, and detailed displays of dependencies) long before adding
various AJAX or other interactive or WYSIWYG features.
> One of the issues that the wiki design has to tackle is ensuring the
> consistency of the proofs. This means that if someone has proven a
> theorem (which typically is a lot of work), then the theorem should
> not stop being valid just because someone decided to modify something
> that the theorem depends on. The previous formalized mathematics wiki
> concepts tried to design an elaborate version control schemes, where
> the theorem would be valid in the context of a specific version of the
> theorem database present at the moment it was verified. The problem
> with this solution is that it would probably require a custom wiki
> I would like to suggest a less ambitious solution: identify all
> operations that may result in inconsistency and ban them.
I agree that your less ambitious solution is a great place to start.
For reference, slides 14-39 of
outline several more complicated possibilities.
Though things along these lines might not be too hard to implement
using a revision control system (as Hendrik Boom suggests).
For now, it is probably best to just get started using a simple
scheme that ensures consistency, and then migrate to allow more
sophisticated operations later.
> Can people start contributing code to the backend, or are we still at
> the drawing board? Is there some document that summarizes the current
> ideas for the structure/organization of the vdash system?
I've posted some additional explanation to the website: http://vdash.org/
I've been working on getting a very basic first version ready
(Monotone + ikiwiki + IsarMathLib, with Isabelle connected
by a simple script which will soon be replaced by a more
robust queue system). Then people can start experimenting
with development ideas on their own, by cloning the repository
and making ikiwiki plugins, CSS, &c.