Abstract
Formalized mathematics currently does not look much like informal mathematics. Also, formalizing mathematics currently seems far too much work to be worth the time of the working mathematician. To address both of these problems we introduce the notion of a formal proof sketch. This is a proof representation that is in between a fully checkable formal proof and a statement without any proof at all. Although a formal proof sketch is too high level to be checkable by computer, it has a precise notion of correctness (hence the adjective formal).
We will show through examples that formal proof sketches can closely mimic already existing mathematical proofs. Therefore, although a formal proof sketch contains gaps in the reasoning from a formal point of view (which is why we call it a sketch), a mathematician probably would call such a text just a ‘proof’.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Asperti, A., Wegner, B.: MOWGLI – A New Approach for the Content Description in Digital Documents. In: Proc. of the 9th Intl. Conference on Electronic Resources and the Social Role of Libraries in the Future, Autonomous Republic of Crimea, Ukraine, vol. 1 (2002)
Cairns, P., Gow, J.: A Theoretical Analysis of Hierarchical Proofs. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 175–187. Springer, Heidelberg (2003)
Hardy, G.H., Wright, E.M.: An Introduction to the Theory of Numbers, 4th edn. Clarendon Press, Oxford (1960)
Harrison, J.: Optimizing Proof Search in Model Elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 313–327. Springer, Heidelberg (1996)
Lamport, L.: How to Write a Proof. American Mathematical Monthly 102(7), 600–608 (1995)
Muzalewski, M.: An Outline of PC Mizar. Fondation Philippe le Hodey, Brussels (1993), http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz
Nederpelt, R.: Weak Type Theory, a formal language for mathematics. Technical Report 02-05, Eindhoven University of Technology, Department of Math. and Comp. Sc. (May 2002)
Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) Proc. 12th Conference on Automated Deduction CADE, Nancy/France, pp. 252–266. Springer, Heidelberg (1994)
Syme, D.: Three Tactic Theorem Proving. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 203–220. Springer, Heidelberg (1999)
Théry, L.: Formal Proof Authoring: an Experiment. In: Lüth, C., Aspinall, D. (eds.) UITP 2003, Rome, Technical Report No. 189, Institut für Informatik, Albert-Ludwigs Universität, Freiburg, September 2003, pp. 143–159 (2003)
Wenzel, M.: Isabelle/Isar — a versatile environment for human-readable formal proof documents. PhD thesis, Institut für Informatik, Technische Universität München (2002), http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html
Wiedijk, F.: Mizar: An Impression (1999), http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz
Wiedijk, F.: Formal proof sketches. In: Fokkink, W., van de Pol, J. (eds.) 7th Dutch Proof Tools Day, Program + Proceedings, Amsterdam (2003), CWI, http://www.cs.kun.nl/~freek/notes/sketches.ps.gz
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wiedijk, F. (2004). Formal Proof Sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds) Types for Proofs and Programs. TYPES 2003. Lecture Notes in Computer Science, vol 3085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24849-1_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-24849-1_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22164-7
Online ISBN: 978-3-540-24849-1
eBook Packages: Springer Book Archive