Abstract:

Lean是一种函数式编程语言，同时也可以作为一种交互式定理证明器. 通过Lean，我们能够将数学直觉转化为形式化的逻辑论证. 我们将介绍通过Lean证明定理的基本方法和一些简单的lean的工作原理.