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

[forecasting]

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

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

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

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

教程视频

[TheMatrix]

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

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

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

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

教程视频

这个听说过。Terrence Tao用这个证明过一个数学定理。是已有的证明，又用这个来重新写了一遍。

[TheMatrix]

[TheMatrix]

大模型说的就是LLM。

输入的是知识，得到的是总结 - 这是合理的。

输入的是知识，得到的是推理，这似乎不是它应该做的。这也能做的话，有点too good to be true的意思。

[forecasting]

大模型说的就是LLM。

输入的是知识，得到的是总结 - 这是合理的。

输入的是知识，得到的是推理，这似乎不是它应该做的。这也能做的话，有点too good to be true的意思。

想说啥？

我只介绍一个验证和证明的工具。

[TheMatrix]

想说啥？

我只介绍一个验证和证明的工具。

是对这句话的评论：