Re: [mizar] "The QED Project"

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

Hi Josef,

Thanks for your interesting comments, which I also forwarded
to Arnold.

>That is the other attractive and probably very productive
>thing about the original idea of Wiki: it is never
>"finished" and "stable", and tries to be very friendly to
>fresh solutions.

I'm not sure I agree with this, not if you are talking about
Wikipedia.

To me that seems very stable both in its _style_ and in its
_look and feel._  The only thing that is being updated all
the time is the _content._  And even then you have a whole
crowd of Wikipedians breathing down your neck (is that an
expression in English?), "stabilizing" what you do.

If you take this approach to formal math, it would mean
that the _style_ and _look and feel_ of formal mathematics
would have to be _very_ stable.

Also, the great strength of Wiki is its simplicity.
Wiki markup for example is very simple, no?  I wish we had
this kind of simplicity in the world of formal math...

Freek