zbMATH — the first resource for mathematics

Proof assistants: history, ideas and future. (English) Zbl 1192.68629
Summary: In this paper I will discuss the fundamental ideas behind proof assistants: What are they and what is a proof anyway? I give a short history of the main ideas, emphasizing the way they ensure the correctness of the mathematics formalized. I will also briefly discuss the places where proof assistants are used and how we envision their extended use in the future. While being an introduction into the world of proof assistants and the main issues behind them, this paper is also a position paper that pushes the further use of proof assistants. We believe that these systems will become the future of mathematics, where definitions, statements, computations and proofs are all available in a computerized form. An important application is and will be in computer supported modelling and verification of systems. But there is still a long road ahead and I will indicate what we believe is needed for the further proliferation of proof assistants.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] ACL2: A Computational Logic/Applicative Common Lisp. http://www.cs.utexas.edu/moore/acl2/Agda : An interactive proof editor. http://agda.sf.net · Zbl 1066.68120
[2] Aigner, Ziegler M G 2004 Proofs from THE BOOK, 3rd ed., Springer
[3] Alur R, Dang T, Ivancic F 2006 Predicate abstraction for reachability analysis of hybrid systems. In: ACM Transactions on Embedded Computing Systems (TECS) 5(1): 152–199 · Zbl 05452341
[4] Asperti A, Geuvers H, Loeb I, Mamane L, Sacerdoti Coen C 2006 An Interactive Algebra Course with Formalised Proofs and Definitions. In: Proceedings of the Fourth Conference Mathematical Knowledge Management, MKM 2005 LNAI 3863, Springer 315–329 · Zbl 1151.97300
[5] Asperti A, Guidi F, Sacerdoti Coen C, Tassi E, Zacchiroli S 2006 A content based mathematical search engine: Whelp. In: Types for Proofs and Programs International Workshop 2004, J-C Filliatre, C Paulin-Mohring, B Werner, (eds), LNCS 3839, Springer 17–32
[6] Avigad J, Donnelly K, Gray D, Raff P 2007 A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic 9(1:2)
[7] Aydemir B, Bohannon A, Fairbairn M, Foster J, Pierce B, Sewell P, Vytiniotis D, Washburn G, Weirich S, Zdancewic S 2005 Mechanized Metatheory for the Masses: The PoplMark Challenge. In Theorem Proving in Higher Order Logics, LNCS 3603, Springer 50–65. Also on (POPLmark) · Zbl 1152.68516
[8] Barendregt H 2003 Towards an Interactive Mathematical Proof Language. In: Thirty Five Years of Automath, Ed. F Kamareddine, (Dordrecht, Boston: Kluwer Academic Publishers) 25–36 · Zbl 1063.68088
[9] Barendregt H, Geuvers H 2001 Proof Assistants using Dependent Type Systems. In: A Robinson, A Voronkov, (eds) Handbook of Automated Reasoning (Vol. 2), Elsevier 1149–1238 (chapter 18) · Zbl 1005.03011
[10] Barras B 1999 Auto-validation d’un vérificateur de preuves avec familles inductives. Ph.D. thesis, Université Paris 7
[11] Blazy S, Dargaye Z, Leroy X 2006 Formal verification of a C compiler front-end. In: FM 2006: Int. Symp. on Formal Methods, LNCS 4085, Springer 460–475
[12] Boyer R S, Moore J S 1998 A Computational Logic Handbook. Second Edition, Academic Press · Zbl 0655.68117
[13] Constable R L, Allen S F, Bromley H M, Cleaveland W R, Cremer J F, Harper R W, Howe D J, Knoblock T B, Mendler N P, Panangaden P, Sasaki J T, Smith S F 1986 Implementing Mathematics with the Nuprl Development System. (NJ: Prentice-Hall)
[14] Corbineau P, Kaliszyk C 2007 Cooperative Repositories for Formal Proofs. In Towards Mechanized Mathematical Assistants, M Kauers et al (eds), LNCS 4573, Springer 221–234 · Zbl 1202.68377
[15] Corbineau P 2007 A declarative proof language for the Coq proof assistant. In Types for Proofs and Programs, LNCS 4941
[16] The Coq proof assistant, http://coq.inria.fr/ · Zbl 1342.68280
[17] Cruz-Filipe L, Geuvers H, Wiedijk F 2004 C-CoRN, the Constructive Coq Repository at Nijmegen. In: A Asperti, G Bancerek, A Trybulec, (eds) Mathematical Knowledge Management, Proceedings of MKM 2004, LNCS 3119, Springer 88–103 · Zbl 1108.68586
[18] De Bruijn N 1983 Automath, a language for mathematics, Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05, 1968. Reprinted in revised form, with two pages commentary. In: Automation and Reasoning, vol. 2, Classical papers on computational logic 1967–1970, Springer Verlag 159–200
[19] Fitch F B 1952 Symbolic Logic, An Introduction, The Ronald Press Company · Zbl 0049.00504
[20] The Flyspeck project, http://www.math.pitt.edu/thales/flyspeck/
[21] Geuvers H, Mamane L 2006 A Document-Oriented Coq Plugin for TeXmacs. In: Libbrecht P, editor, Proceedings of the MathUI workshop at the MKM 2006 conference, Wokingham, UK, http://www.activemath.org/paul/MathUI06/
[22] Gonthier G 2004 A computer-checked proof of the Four Colour Theorem, http://research.microsoft.com/gonthier/4colproof.pdf
[23] Gordon M J C 2006 From LCF to HOL: a short history. Proof, language, and interaction: essays in honour of Robin Milner (Cambridge, MA, USA: MIT Press) 169–185, 2000
[24] Gordon M J C, Melham T F 1993 Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press · Zbl 0779.68007
[25] Gordon M J C, Milner R, Wadsworth C P 1979 Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag
[26] Hales Th 2007 A proof of the Kepler conjecture. In: Annals of Mathematics 162: 1065–1185 · Zbl 1096.52010
[27] Hales Th 2007 Jordan’s Proof of the Jordan Curve Theorem. In From Insight to Proof Festschrift in Honour of Andrzej Trybulec (eds) R Matuszewski, A Zalewska, Studies in Logic, Grammar and Rhetoric 10(23)
[28] Halmos P 1985 I want to be a Mathematician: An Automathography, Springer 410
[29] Harper R, Honsell F, Plotkin G 1993 A framework for defining logics. Journal of the ACM 40: 194–204 · Zbl 0778.03004
[30] Harrison J 1996 A Mizar Mode for HOL, Proceedings, of Theorem Proving in Higher Order Logics, TPHOLs’96, Turku, Finland, Lecture Notes in Computer Science 1125, Springer 203–220
[31] Harrison J 2000 Formal verification of IA-64 division algorithms, in: M Aagaard, J Harrison, (eds), Theorem Proving in Higher Order Logics, TPHOLs 2000 LNCS 1869, Springer 234–251 · Zbl 0974.68535
[32] Harrison J 2006 Towards self-verification of HOL Light, U Furbach, N Shankar (eds), Proceedings of the Third International Joint Conference IJCAR 2006, Seattle, WA, LNCS 4130, 177–191
[33] The HOL Light theorem prover http://www.cl.cam.ac.uk/jrh13/hol-light/HOL4 , http://hol.sourceforge.net/
[34] Howard W A 1980 The formulae-as-types notion of construction, in J Seldin, R Hindley (eds), to H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston, MA, Academic Press, 479–490, (original manuscript from 1969)
[35] Isabelle, http://isabelle.in.tum.de/
[36] Jaśkowski S 1967 On the rules of suppositional formal logic. In Storrs McCall, editor, Polish Logic 1920–1939 232–258. (Oxford: Clarendon Press)
[37] Kaliszyk C 2007 Web Interfaces for Proof Assistants, Electr. Notes Theor. Comput. Sci. 174(2): 49–61
[38] Kaufmann M, Manolios P, Moore J S 2000 Computer-Aided Reasoning: An Approach Kluwer Academic Publishers
[39] Knuth D 1992 Literate Programming, Center for the Study of Language and Information, 1992, xvi+368pp. CSLI Lecture Notes, no. 27, Stanford, California
[40] Kohlhase M 2000 OMDoc: Towards an Internet Standard for the Administration, Distribution and Teaching of mathematical Knowledge, in Proceedings of Artificial Intelligence and Symbolic Computation, Springer LNAI · Zbl 1042.00511
[41] Korniłowicz A 2005 Jordan curve theorem. Formalized Mathematics 13(4): 481–491
[42] Letouzey P 2003 A new extraction for Coq. Proceedings of the TYPES Conference 2002, LNCS 2626, Springer-Verlag 200–219
[43] Lyaletski A, Paskevich A, Verchinin K 2004 Theorem Proving and Proof Verification in the System SAD. In: Mathematical Knowledge Management, Third International Conference, Białowieza, Poland, Proceedings, LNCS 3119, 236–250
[44] Luo Z, Pollack R 1992 LEGO Proof Development System: User’s Manual, LFCS Technical Report ECS-LFCS-92-211
[45] Magnusson L, Nordström B 1994 The ALF proof editor and its proof engine, In Types for Proofs and Programs, H Barendregt, T Nipkow (eds), LNCS, 806: 213–237
[46] Martin-Löf P 1984 Intuitionistic type theory, Napoli, Bibliopolis
[47] Matuszewski R, Rudnicki P 2005 Mizar: the first 30 years, Mechanized mathematics and its applications 4(1): 3–24
[48] McCarthy J 1962 Computer programs for checking mathematical proofs, In Recursive Function Theory, Proceedings of Symposia in Pure Mathematics, volume 5. Americal Mathematical Society · Zbl 0143.40007
[49] Mizar Home Page, http://www.mizar.org/
[50] Muñoz C, Dowek G 2005 Hybrid Verification of an Air Traffic Operational Concept, in: Proceedings of IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation, Columbia, Maryland
[51] Necula G, Lee P 1996 Proof-Carrying Code, Technical Report CMU-CS-96-165, November 1996. (62 pages) http://www.cs.berkeley.edu/necula/Papers/tr96-165.ps.gz
[52] Nederpelt R P, Geuvers H, de Vrijer R C 1994 (editors), Selected Papers on Automath, Volume 133 in Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, pp 1024 · Zbl 0822.03009
[53] Nordström B, Petersson K, Smith J 1990 Programming in Martin-Löf’s Type Theory Oxford University Press · Zbl 0744.03029
[54] The OpenMath Society, http://www.openmath.org/
[55] OMDoc, A Standard for Open Mathematical Documents, http://www.mathweb.org/omdoc/
[56] Paulin-Mohring Ch 1989 Extracting F{\(\omega\)}’s programs from proofs in the Calulus of Constructions, Sixteenth Annual ACM Symposium on Principles of Programming Languages, ACM, Austin
[57] The POPLmark Challenge.s http://fling-l.seas.upenn.edu/plclub/cgi-bin/poplmark · Zbl 1152.68516
[58] PVS Specification and Verification System http://pvs.csl.sri.com/
[59] The QED Manifesto, in: Automated Deduction – CADE 12, LNAI 814, Springer, 1994, 238–251
[60] Scott D 1993 A type-theoretical alternative to ISWIM, CUCH, OWHY. TCS, 121: 411–440, 1993. (Annotated version of a 1969 manuscript) · Zbl 0942.68522
[61] Scott D 1970 Constructive validity. Symposium on Automatic Demonstration (Versailles, 1968), Lecture Notes in Mathematics, Vol. 125, Springer, Berlin 237–275
[62] TeXmacs, http://www.math.u-psud.fr/anh/TeXmacs/TeXmacs.html
[63] The Twelf Project, http://twelf.plparty.org/
[64] Verchinine K, Lyaletski A, Paskevich A, Anisimov A 2008 On correctness of mathematical texts from a logical and practical point of view. In: Intelligent Computer Mathematics, AISC/Calculemus/MKM 2008, Birmingham, UK, LNCS 5144, Springer 583–598 · Zbl 1166.68353
[65] Wagner M, Dietrich D, Schulz E 2008 Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors, In Intelligent Computer Mathematics, AISC/Calculemus/MKM 2008, Birmingham, UK, LNCS 5144, Springer · Zbl 1166.68342
[66] Wenzel M, Paulson LC, Nipkow T 2008 The Isabelle Framework. In:O Ait-Mohamed, editor, Theorem Proving in Higher Order Logics, TPHOLs 2008, invited paper, LNCS 5170 Springer · Zbl 1165.68478
[67] Wenzel M 2006 Isabelle/Isar – a generic framework for human-readable proof documents. In R Matuszewski and A Zalewska, (eds) From Insight to Proof – Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric 10(23), University of Białystok
[68] Wiedijk F 2004 Formal Proof Sketches, In Types for Proofs and Programs: Third International Workshop, TYPES 2003. In: S Berardi, M Coppo, F Damiani, (eds), Springer, LNCS 3085 378–393
[69] Wiedijk F 2005 Estimating the Cost of a Standard Library for a Mathematical Proof Checker, http://www.cs.ru.nl/freek/notes/index.html
[70] Wiedijk F 2006 (ed.) The Seventeen Provers of the World, Springer LNAI 3600 · Zbl 1114.03007
[71] Wiedijk F 2008 Formalizing the ’top 100’ of mathematical theorems http://www.cs.ru.nl/freek/100/index.html
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.