MathWiki initiatives in Europe
geu...@gmail.com
A very interesting project vdash!
A very similar idea and project proposal has come up recently in
Europe. I would like to point out the webpage http://prover.cs.ru.nl/wiki.php
where it is all summarized:
- We (at Radboud University Nijmegen, NL) have a web interface for
proof assistants that now supports Coq and Isabelle/HOL and gives
preliminary support to other proof assistants. You can experiment with
it.
- We plan to extend this to a MathWiki system that should
+ support cooperative work on a shared repository by PA users
through a web interface
+ support the creation of high level pages for describing
mathematical content, with direct links to the formal content.
+ support the linking between "the same" objects in different proof
assistant repositories. (What does the binomial look like in
Isabelle?)
+ support meaningful search for mathematical content and meaningful
mathematical objects in the web pages.
- We have applied for a EU project (together with Paris, Edinburgh, TU
Munich, Bialystok Poland, Bremen and Bologna), but it failed to get
funded.
- There has been a small MathWiki workshop in Edinburgh in the autumn
of 2007: http://homepages.inf.ed.ac.uk/da/mathwiki/
Please let me know what you think. I guess it would be good to
cooperate on this, not to double the efforts.
Best Regards
Herman Geuvers
Radboud University Nijmegen
The Netherlands
Cameron Freer
Prof. Geuvers,
Thanks for getting in touch! I've meaning to contact you and your
group. I've been aware of your project for a few months, and after
TPHOLs this summer, John Harrison pointed me towards ProofWeb (after
Freek Wiedijk reminded him).
In particular, there are some great ideas in
http://hair-dryer.cs.ru.nl/~cek/docs/cek_p6.pdf
and
http://hair-dryer.cs.ru.nl/~cek/docs/cek_p3.pdf
It'd be great to work together, both to share ideas and not
duplicate efforts.
I suspect that our long-range goals are very similar. In the
shorter-term, I had a somewhat different approach in mind:
1. I think it's very important that the lowest visible layer still
be a human-readable proof, and not just a proof script with an
informal layer on top. Hence I think Isar (or, e.g., declarative
mode in Coq, or Mizar Light for HOL Light) is essential. Comments
in the code can help to explain things, but if we have an informal
layer with a disconnected obscure layer of code below it, we're not
taking full advantage of the power of formalization.
2. Even though HOL or Coq (or other systems based on type-theory or
the CoC) currently have the most momentum for pure math, I think
that in the long run, things will be most naturally implemented in
ZF (with better methods than currently exist for abstracting away
the lower layer, for results beyond basic set theory).
3. It'd be great to eventually link up Coq, HOL4, HOL Light, Matita,
Lego, Plastic, Isabelle/HOL, Isabelle/ZF, &c. (with their
corresponding piles of already formalized math), but at this point I
think that may be more of a distraction from the goal of building up
a sizable repository. Also, I think the end goal (within the
domain of pure math, at least) should be something like a single
good language choice, with results imported from elsewhere (so long
as they are still natively readable in the common language.
For all of these reasons, I think Isabelle/ZF, with proofs in a
readable and annotated Isar style, is the correct choice. For
example, the style in Slawekk's IsarMathLib is close to ideal, and I
think it would be a great starting point of results in a common format:
http://savannah.nongnu.org/projects/isarmathlib
http://www.nongnu.org/isarmathlib/
(Mizar somewhat fits in with the above goals, but (in part) for reasons
of software architecture and openness, I think it is not optimal.)
4. I generally feel that having an interactive AJAX interface for
the theorem prover is less essential than having a language/format
which facilitates quick simple edits, and also encourages proof
sketches, as in
http://www.in.tum.de/~wenzelm/papers/romantic.pdf
The ease of outlining proofs (via "sorry" in Isar, e.g.) seems key
to allowing top-down development, which is one of the most exciting
possibilities enabled by a wiki. That said, I think interactive
web features are just a matter of time, so this may just be a
question of ordering priorities.
In what directions do you think we might collaborate? I can picture
that your current ProofWeb interface for Isabelle/ZF could usefully
be hooked in to the wiki database as a sort of sandbox for
prototyping documents, and as many users' preferred interface for
longer edits. Also, your basic software architecture plan seems
very reasonable (as laid out in
http://www.cs.ru.nl/~herman/TALKS/slides-RU-coll.pdf
and the second PDF link above). How do you suggest we proceed?
Best,
- Cameron
--------------------------------------
Cameron Freer
Department of Mathematics
Massachusetts Institute of Technology
Cambridge, MA