Panel discussion: A mechanically proof-checked Encyclopedia of Mathematics: Should we build one? can we?

Abstract

At the suggestion of the CADE-12 Program Committee Chairman, Professor Alan Bundy, a panel discussion on the topic “A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We?” has been organized, with participants Robert S. Boyer, N. G. de Bruijn, Gérard Huet, and Andrzej Trybulec. This discussion will consider an idea, a vision, that has been shared and pursued by a number of groups for at least several decades, an idea that is also described in the following, anonymously authored document The QED Manifesto, which has been influenced by contributions and criticisms from numerous quarters.