陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看

[VladPutin]

https://github.com/teorth/analysis

The files in this directory contain a formalization of selected portions of my text Analysis I into Lean. The formalization is intended to be as faithful a paraphrasing as possible to the original text, while also showcasing Lean's features and syntax. In particular, the formalization is not optimized for efficiency, and in some cases may deviate from idiomatic Lean usage.

[Caravel]

陶要投降机器了

[heteroclinic]

挺好,就是字体太单调,失去了磨扎克的优雅,用草书就好了.
陶贤弟是一众LLM公认当世第一的数学家!

[mingliu]

看到“福利”，兴冲冲地跑进来，就给我看这个？！

[forecasting]

https://github.com/teorth/analysis

The files in this directory contain a formalization of selected portions of my text Analysis I into Lean. The formalization is intended to be as faithful a paraphrasing as possible to the original text, while also showcasing Lean's features and syntax. In particular, the formalization is not optimized for efficiency, and in some cases may deviate from idiomatic Lean usage.

Tao在做工程。
你觉得用Lean写数学证明很了不起？

[VladPutin]

Tao在做工程。
你觉得用Lean写数学证明很了不起？

不知道，据说很有用。

[forecasting]

不知道，据说很有用。

把证明转换成Lean语言的形式，现在不困难，尤其Tao发动一帮数学家做等式项目可以作为Lean语言的库。Lean说白了就是直觉逻辑的实现，换言之，就是把人做的证明转换成直觉逻辑的证明，现在有不少辅助工具，工作量不那么大。转换之后可以运行以检验原来的人工证明是否正确，前提是Lean语言的证明和人工证明等价，有时候转换会出问题，得小心检查或者debug。

[wdong]

我认为没用。具体在下面的帖子里。

http://xhslink.com/a/x1z34qlNx8cfb

[forecasting]

我认为没用。具体在下面的帖子里。

http://xhslink.com/a/x1z34qlNx8cfb

直觉如此，可得证明啊。

你在忙啥，还在做那agent？

[heteroclinic]

苏联笑话
废纸篓里三张废纸在白话
A : 我支持AI
B : 我反对AI
C : 我就是AI

[TheMatrix]

我认为没用。具体在下面的帖子里。

http://xhslink.com/a/x1z34qlNx8cfb

看了。说的非常有道理。

[wdong]

直觉如此，可得证明啊。

你在忙啥，还在做那agent？

我现在主要在小红书发帖，看的人比较多。

[forecasting]

我现在主要在小红书发帖，看的人比较多。

这是要做大V，会成为网红的。