Re: "The QED Project"

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: <[email protected]>
> Date: Tue, 20 Jan 2009 14:12:20 +0100
> From: Arnold Neumaier <[email protected]>
> To: Freek Wiedijk <[email protected]>
> 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/
> ----------------------------------------------------------------
>