（转载）交互数学定理自动证明器，验证器与数学证明语言（器）

[forecasting]

此帖转自 forecasting 在 STEM 的帖子：交互数学定理自动证明器，验证器与数学证明语言（器）

此证明，验证语言（器）是从lisp，prolog和类型论，直觉逻辑以及一些前期的机器证明器（语言）发展而来。

官网
https://lean-lang.org/

教程
https://brandonrozek.com/blog/lean3-tutorial/

https://www.ma.imperial.ac.uk/~buzzard/ ... orial.html

教程视频