The Lean Theorem Prover (System Description)

被引：213
作者：
de Moura, Leonardo [1 ]
Kong, Soonho [2 ]
Avigad, Jeremy [2 ]
van Doorn, Floris [2 ]
von Raumer, Jakob [2 ]
机构：
[1] Microsoft Res, Redmond, WA 98052 USA
[2] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
来源：
AUTOMATED DEDUCTION - CADE-25 | 2015年 / 9195卷
关键词：
CONSTRUCTIONS;
D O I：
10.1007/978-3-319-21401-6_26
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
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.
引用
收藏
页码：378 / 388
页数：11
相关论文
共 24 条
[1]  
[Anonymous], 2013, Homotopy type theory: univalent foundations of mathematics
[2]  
Asperti A, 2011, LECT NOTES ARTIF INT, V6803, P64, DOI 10.1007/978-3-642-22438-6_7
[3]  
Avigad J., 2015, THEOREM PROVING LEAN, V3, P1
[4]  
Barras Bruno, 1997, The Coq proof assistant reference manual: Version 6.1
[5]  
Cockx J., 2014, P 19 ACM SIGLPLAN IN, P257
[6]   THE CALCULUS OF CONSTRUCTIONS [J].
COQUAND, T ;
HUET, G .
INFORMATION AND COMPUTATION, 1988, 76 (2-3) :95-120
[7]  
COQUAND T, 1990, LECT NOTES COMPUT SC, V417, P50
[8]  
de Moura L., ELABORATION DEPENDEN
[9]  
Dybjer P., 1994, Formal Aspects of Computing, V6, P440, DOI 10.1007/BF01211308
[10]  
Goguen H, 2006, LECT NOTES COMPUT SC, V4060, P521, DOI 10.1007/11780274_27
123