新未名空间

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

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

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

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

教程视频

forecasting 写了： 2024年 11月 23日 04:56 此证明，验证语言（器）是从lisp，prolog和类型论，直觉逻辑以及一些前期的机器证明器（语言）发展而来。

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

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

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

教程视频

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

TheMatrix 写了： 2024年 11月 23日 12:56

大模型说的就是LLM。

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

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

TheMatrix 写了： 2024年 11月 23日 13:48 大模型说的就是LLM。

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

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

想说啥？

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

forecasting 写了： 2024年 11月 23日 13:52 想说啥？

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

是对这句话的评论：

TheMatrix 写了： 2024年 11月 23日 12:56