10.6092/issn.1972-5787/5974
This special issue is dedicated to the 20th anniversary of the QEDManifesto and the related 1994 and 1995 QED Workshops.
application/pdf
1972-5787
5974
1
en
Freek Wiedijk
Journal of Formalized Reasoning
formalization of mathematics
Preface: Twenty Years of the QED Manifesto
Text.Serial.Journal
https://jfr.unibo.it/
9
QED 20th anniversary
2016-01-29
2016-01-26
2016-01-29
2016-12-23
1 - 2
JFR
Freek Wiedijk
2016/01/29
10.6092/issn.1972-5787/5974
1
1972-5787
1
formalization of mathematics
en
2
Preface: Twenty Years of the QED Manifesto
https://jfr.unibo.it/article/download/5974/5759
9
Preface: Twenty Years of the QED Manifesto
John Harrison, Josef Urban and Freek Wiedijk


This special issue is dedicated to the 20th anniversary of the QED Manifesto and the related 1994
and 1995 QED Workshops.1




  The following is a short excerpt from the QED Manifesto:2
      QED is the very tentative title of a project to build a computer system
      that effectively represents all important mathematical knowledge and
      techniques. The QED system will conform to the highest standards of
      mathematical rigor, including the use of strict formality in the internal
      representation of knowledge and the use of mechanical methods to check
      proofs of the correctness of all entries in the system. . .
   This special issue was preceded by a one-day QED+20 workshop3 taking place
in Vienna on July 18, 2014, as a part of the Vienna Summer of Logic. Our main
goal was to show on real formal developments the state of the art in formalization
of mathematics 20 years after QED. We also wanted to remember and discuss QED
and its goals, to see how we are (not yet) achieving them, and what are the current
issues and their proposed/prototyped/working solutions.
   The workshop indeed managed to pack – and perhaps overpack – into one day
talks about the greatest achievements in formalization done since QED. It started
with John Harrison’s personal memories of the QED discussions and workshops, his
assessment of the successes and failures of QED-style efforts, followed by a lively
discussion. Georges Gonthier then gave an overview of his famous formalizations
on the Four Color theorem and Odd Order theorem, commenting on their his-
tory and links between them. This opulent morning series continued with Adam
Grabowski’s overview of the formalizations done in the Mizar Mathematical Li-
brary, Gerwin Klein’s hands-on talk of the breakthrough project verifying the seL4
microkernel in Isabelle, Magnus Myreen’s and Ramana Kumar’s talks about their
work taking verification of theorem provers and their implementation languages to
dizzying depths, and Claudio Sacerdoti Coen’s note on the current state and future
of extension languages for theorem provers.
   The afternoon session ran in a similar spirit. It started with Tom Hales’ talk
about his groundbreaking Flyspeck project, which was completed just a few weeks
after the talk. It continued with talks by Michael Beeson – describing his own
approach and those of others to the crucial topic of mixing computations and rea-
soning, Marcos Cramer’s talk on proof-checking mathematical texts in controlled
natural language, Geoff Sutcliffe’s talk showing the QED-style opportunities al-
ready happening in his well-integrated World of TPTP, Michael Kohlhase’s well-

2 http://www.cs.ru.nl/
                         ~freek/qed/qed.html
3 http://www.cs.ru.nl/qed20/



                                         Journal of Formalized Reasoning Vol. 9, No. 1, 2016 Pages 1–2.
2     ·     John Harrison, Josef Urban, Freek Wiedijk

argued call for flexiformality as a necessary bridge between informal and formal,
and Cezary Kaliszyk’s overview of today’s large-theory automated theorem proving
methods and their impressive performance. The workshop closed by a short panel
discussion, continued further at the workshop dinner.
   This special issue contains nine papers on various QED topics, either expanding
on some of the QED talks, or discussing related topics and proof assistants, some
of them complementing today’s formalization mainstream.
   Three papers – one by Michael Beeson, one by Michael Kohlhase and Florian
Rabe, and one by Jasmin Blanchette, Cezary Kaliszyk, Larry Paulson and Josef
Urban – expand on their respective QED talks. Mark Adams’ paper discusses
the topic of auditing formal mathematics, and announces the cross-verification of
the formalization of the textual part of the Flyspeck project. Rob Arthan’s paper
describes a generic automation procedure for showing that a given function is a
morphism in some category. Arnon Avron’s and Liron Cohen’s paper proposes a
new definitional framework based on set-theory for formalization. The paper by
Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, and Wolf-
gang Windsteiger presents the new version of the Theorema proof assistant. Mario
Carneiro’s paper is about translating proofs between HOL Light and OpenTheory
and the Metamath system, and Alexander Lyaletski’s paper describes the Evidence
Algorithm project and its history, and discusses one of its particular aspects.
   We are very happy with the way the QED+20 workshop and this special issue
have turned out. The workshop has shown to us that there still is a large interest
in the goals of the original QED Manifesto.
   Twenty years on, can we say anything about the success of the QED project? In
the most obvious sense, the project did not succeed at all. The QED list discussion
tailed off with no more workshops and there is no unified “QED system”. Despite
a number of attempts, there is not much use of metalogics to share results. If any-
thing, Balkanization has got even worse. A more positive view is that QED had
many positive side-effects like bringing Mizar and other theorem proving groups to-
gether. There has been substantial progress over 20 years in formalizing non-trivial
theorems and improving systems. We also have a number of working approaches
for sharing proofs between theorem-proving systems – some of them described in
this special issue.
   We think that the spirit of the original QED Manifesto is not dead at all. We
hope that the QED+20 workshop and this special issue are modest contributions
to a very interesting future – perhaps the “QED Singularity” as Michael Beeson’s
paper calls it – in which many of the original QED ideas will be realized.




Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
