Skip to main content
Top

2015 | OriginalPaper | Chapter

The Lean Theorem Prover (System Description)

Authors : Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer

Published in: Automated Deduction - CADE-25

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort, but it already provides many useful components, integrated development environments, and a rich API which can be used to embed it into other systems. It is currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe the project goals, system architecture, and main features, and we discuss applications and continuing work.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita interactive theorem prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64–69. Springer, Heidelberg (2011) CrossRef Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita interactive theorem prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64–69. Springer, Heidelberg (2011) CrossRef
3.
go back to reference Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C. et al.: The Coq proof assistant reference manual: Version 6.1 (1997) Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C. et al.: The Coq proof assistant reference manual: Version 6.1 (1997)
4.
go back to reference Cockx, J., Devriese, D., Piessens, F.: Pattern matching without K. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 257–268. ACM (2014) Cockx, J., Devriese, D., Piessens, F.: Pattern matching without K. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 257–268. ACM (2014)
6.
go back to reference Coquand, T., Paulin, C.: Inductively defined types. In: COLOG-88 (Tallinn, 1988), pp. 50–66. Springer, Berlin (1990) Coquand, T., Paulin, C.: Inductively defined types. In: COLOG-88 (Tallinn, 1988), pp. 50–66. Springer, Berlin (1990)
7.
go back to reference de Moura, L., Avigad, J., Kong, S., Roux, C.: Elaboration in dependent type theory. Preprint (arXiv) de Moura, L., Avigad, J., Kong, S., Roux, C.: Elaboration in dependent type theory. Preprint (arXiv)
8.
go back to reference Delahaye, D., Woltzenlogel Paleo, B. (eds.): All about proofs, proofs for all. Mathematical Logic and Foundations, vol. 55 (2015) Delahaye, D., Woltzenlogel Paleo, B. (eds.): All about proofs, proofs for all. Mathematical Logic and Foundations, vol. 55 (2015)
10.
go back to reference Goguen, H.H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 521–540. Springer, Heidelberg (2006) CrossRef Goguen, H.H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 521–540. Springer, Heidelberg (2006) CrossRef
11.
go back to reference Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009) CrossRef Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009) CrossRef
12.
go back to reference Martin-Löf, P.: Intuitionistic type theory. Bibliopolis (1984) Martin-Löf, P.: Intuitionistic type theory. Bibliopolis (1984)
13.
go back to reference McBride, C., Goguen, H.H., McKinna, J.: A few constructions on constructors. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 186–200. Springer, Heidelberg (2006) CrossRef McBride, C., Goguen, H.H., McKinna, J.: A few constructions on constructors. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 186–200. Springer, Heidelberg (2006) CrossRef
14.
go back to reference McBride, C., McKinna, J.: Functional pearl: I am not a number-I am a free variable. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell 2004, pp. 1–9. ACM, New York (2004) McBride, C., McKinna, J.: Functional pearl: I am not a number-I am a free variable. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell 2004, pp. 1–9. ACM, New York (2004)
15.
go back to reference Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)CrossRefMATH Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)CrossRefMATH
16.
go back to reference Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, Deepak (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992) Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, Deepak (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)
17.
go back to reference Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283. Springer Science and Business Media (2002) Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283. Springer Science and Business Media (2002)
18.
go back to reference Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009) CrossRef Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009) CrossRef
19.
go back to reference Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Kapur, Deepak (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992) Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Kapur, Deepak (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)
20.
go back to reference Rudnicki, P.: An overview of the Mizar project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311–330 (1992) Rudnicki, P.: An overview of the Mizar project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311–330 (1992)
21.
go back to reference Slind, K.: Function definition in higher-order logic. In: von Wright, Joakim, Harrison, J., Grundy, John (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996) CrossRef Slind, K.: Function definition in higher-order logic. In: von Wright, Joakim, Harrison, J., Grundy, John (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996) CrossRef
22.
go back to reference Streicher, T.: Investigations into intensional type theory. Ph.D. thesis, LMU (1993) Streicher, T.: Investigations into intensional type theory. Ph.D. thesis, LMU (1993)
23.
go back to reference The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013) The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013)
24.
go back to reference Wenzel, M.M.: Isabelle/Isar - a versatile environment for human-readable formal proof documents. Technical report ( 2002) Wenzel, M.M.: Isabelle/Isar - a versatile environment for human-readable formal proof documents. Technical report ( 2002)
Metadata
Title
The Lean Theorem Prover (System Description)
Authors
Leonardo de Moura
Soonho Kong
Jeremy Avigad
Floris van Doorn
Jakob von Raumer
Copyright Year
2015
DOI
https://doi.org/10.1007/978-3-319-21401-6_26

Premium Partner