[FOM] The QED Manifesto today
Roger Bishop Jones
rbj at rbjones.com
Fri Jan 23 03:52:44 EST 2009
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
This is in effect what has happened.
If you look at the page by Freek Wiedijk:
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.
More information about the FOM