Re: [mizar] the Why project

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Josef,

>Question is how to maintain the articles automatically generated by 
>various Why-like projects (if there are any pieces of mathematics worth 
>maintaining in them). It can be either re-generated for newer MML each 
>time, or included in MML and be revised together with MML. I guess these 
>two methods will not always produce the same results. How is this done 
>with the Coq library and the 4-color theorem, or  HOL Light and Flyspeck?

I don't know really.

With Coq there is the "contribs", which is a bit like MML in
the sense that it is updated when the system changes, although
it is not integrated into a whole without duplications like
MML is.  With HOL Light there is not so very much in the first
place, although John _did_ put the most interesting things as
subdirectories in his distribution.

So the 4-color theorem is currently not yet in the Coq
contribs, I think (maybe because of copyright isssues with
Microsoft?  It uses Georges Gonthier's wonderful proof
language, which is a whole technology of its own, really.) The
Jordan Curve Theorem formalization that Tom Hales wrote _is_
part of the HOL Light distribution.

But I don't know how many formalizations based on
automatically generated stuff are in the Coq contribs.  Maybe
work by Laurent Thery?

Freek