[FOM] The QED Manifesto today

[Roger Bishop Jones]

My opinion at the time when QED was active was that the best way to progress 
the technology supporting formal development and application of mathematics 
was by continuing to work with the proof tools already then available.
It seemed to me that we were nowhere near the limits of what could be done by 
continuing to work with those tools, and that inventing new languages and 
building tools to support them would be a distraction from discovering and 
addressing the practical issues involved in the formal development of 
mathematics.

This is in effect what has happened.
If you look at the page by Freek Wiedijk: 

http://www.cs.ru.nl/~freek/100/index.html

You find a list of tools in use for the formalisation of mathematics, together 
with information about how many of the "top 100" theorems they have proved.
I believe that all of those theorem provers was already available at the time 
of the QED project (or is derived from something that was then available);

There have been other initiatives which are relevant to the the objectives of 
QED one cluster of these is the Calculemus project/interest group at 
calculemus.net which may be the closest currently active initiative to the 
objectives of the QED project.

Roger Jones