[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] "The QED Project"



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._


Ok, I'll freely associate a bit more :-).
I think the "content" is what matters (and is difficult) in both wiki and formal math. The "look and feel" (syntax?) is easier. Things like keywords and symbols can be (and are) transformed quite easily by various presentation layers and translations. There is a lot of structure encoded in the wiki "content", and that structure is changing a lot.
Perhaps in some sense wiki is also a bit like the "minikernel" systems like HOL: the "hard-wiring" is quite minimal, and it very much depends on what users build on top of it. 


And even then you have a whole
crowd of Wikipedians breathing down your neck (is that an
expression in English?), "stabilizing" what you do.
I also wonder where it is going. I read somewhere that a huge ratio of WP pages are devoted to WP-administration. Many articles have long talk pages that even exceed the documented article. But things like handling of mathematics, infoboxes, categorization,..., are certainly developing. There are various subprojects taking care of various fields and issues. And even the "stabilization" customs are changing quite a bit too, e.g. the "Deletionist" vs. "Inclusionist" balance has been changing in the recent years. 


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.
I think the superficial "look and feel" might be quite misleading. It seems to me that the WP community has gone through a very interesting process of defining how an article should look, what should be in it and what not in various cases, how to cite and link, when to lock a page and when to kick a user, how the community should govern itself, etc. etc. A lot of discussions and decisions, a lot of discussions about the articles. A lot of new large-scale "cooperative culture". Nothing of this scale in the formal math projects around :-). 


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...
Yes, they have just one basic type check: the link either exists or not :-). And they do not make a big deal from articles that don't type check - eventually, they will :-). But there are many more checks ("bots" and humans) that watch the WP articles in the long run, and making a "good" article in one shot is probably not that simple. 

Josef