"The QED Project"

[Freek Wiedijk]

Dear list members,

A few days ago I got the email copied below.  And I don't
very well know what to say to it.  Does anyone here have
a good answer to Arnold's query?

(I'm cross-posting this to a couple of mailing lists.  So my
excuses for the duplication, but I'm really curious whether
there is anything interesting to say to this question.)

Freek

----------------------------------------------------------------
Message-ID: <4975CDB4.2010107@...>
Date: Tue, 20 Jan 2009 14:12:20 +0100
From: Arnold Neumaier <Arnold.Neumaier@...>
To: Freek Wiedijk <freek@...>
Subject: The QED Project

Freek,

are there still activities related to the QED Project
     http://www-unix.mcs.anl.gov/qed/
I am contemplating writing a grant application for something going
in a similar direction, and would like to know about which people to
contact for possible collaboration.

What is your current assessment of what it takes to realize an
updated version of the QED project?


Best wishes,

Arnold

http://www.mat.univie.ac.at/~neum/
----------------------------------------------------------------

[Josef Urban]

Hi Freek,

The first sentence at http://www-unix.mcs.anl.gov/qed/ is:

"The aim of the QED project is to build a single, distributed,
computerized repository that rigorously represents all important,
established mathematical knowledge."

I think this is a target of multiple projects today - one of them Mizar,
but e.g. all the "semantic wiki for formal math" recent suggestions are
also driven by this goal (and by the huge practical success of Wikipedia,
showing that such things are really possible in a couple of years if
started and coordinated well).

The other point is that no project is sofar nowhere near achieving the
goal. I think that the "goal" should rather be defined as a process that
gradually tries to involve as many mathematicians/students as possible,
and continuously tries to make formalization easier and easier for
newcomers. 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 fear that without such
supportive climate and humble awareness of the huge existing bottlenecks
that are waiting to be solved, no project will succeed.

So I think that in some sense the world is still waiting for the proper
effort towards implementation of QED. We know that it is possible, but it
is both a technical problem, and a human resource management problem.
Especially solving the latter is in my opinion the crucial thing. The only
way how a "technical solution" could be more important than the "human
solution" is if very good tools and AI are developed, which will
practically turn the "normal" mathematical papers into "formal"
mathematical papers. E.g. TeX is an example of a technical solution that
changed the world in a similar sense, and you never know where AI (for
automated formalization of "normal" math) is :-).

Josef

On Thu, 22 Jan 2009, Freek Wiedijk wrote:

> Dear list members,
>
> A few days ago I got the email copied below.  And I don't
> very well know what to say to it.  Does anyone here have
> a good answer to Arnold's query?
>
> (I'm cross-posting this to a couple of mailing lists.  So my
> excuses for the duplication, but I'm really curious whether
> there is anything interesting to say to this question.)
>
> Freek
>
> ----------------------------------------------------------------
> Message-ID: <4975CDB4.2010107@...>
> Date: Tue, 20 Jan 2009 14:12:20 +0100
> From: Arnold Neumaier <Arnold.Neumaier@...>
> To: Freek Wiedijk <freek@...>
> Subject: The QED Project
>
> Freek,
>
> are there still activities related to the QED Project
>     http://www-unix.mcs.anl.gov/qed/
> I am contemplating writing a grant application for something going
> in a similar direction, and would like to know about which people to
> contact for possible collaboration.
>
> What is your current assessment of what it takes to realize an
> updated version of the QED project?
>
>
> Best wishes,
>
> Arnold
>
> http://www.mat.univie.ac.at/~neum/
> ----------------------------------------------------------------
>

[Freek Wiedijk]

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

[Josef Urban]

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

[slawekk]

The http://vdash.org/formal/ page in the section "Other Formalization Efforts" contains a list of current projects related to formalized mathematics.
With some web searching this list can be converted to a list of people to contact.

Slawekk

IsarMathLib (www.formalmath.org)
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

> ----------------------------------------------------------------
> Message-ID: <4975CDB4.2010107@...>
> Date: Tue, 20 Jan 2009 14:12:20 +0100
> From: Arnold Neumaier <Arnold.Neumaier@...>
> To: Freek Wiedijk <freek@...>
> Subject: The QED Project
> would like to know about which
> people to
> contact for possible collaboration.
>