10 views

Skip to first unread message

Oct 10, 2008, 9:00:52 AM10/10/08

to vdash, her...@cs.ru.nl

Dear all,

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

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

Oct 10, 2008, 10:37:59 AM10/10/08

to vdash, her...@cs.ru.nl

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu