分页： 1 / 1
#1 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 4日 14:28
由 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.
#2 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 4日 23:11
由 Caravel
陶要投降机器了
#3 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 5日 16:31
由 heteroclinic
挺好,就是字体太单调,失去了磨扎克的优雅,用草书就好了.
陶贤弟是一众LLM公认当世第一的数学家!
#4 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 6日 12:49
由 mingliu
看到“福利”，兴冲冲地跑进来，就给我看这个？！
#5 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 9日 07:50
由 forecasting
VladPutin 写了： 2025年 6月 4日 14:28
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写数学证明很了不起？
#6 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 13日 13:16
由 VladPutin
forecasting 写了： 2025年 6月 9日 07:50
Tao在做工程。
你觉得用Lean写数学证明很了不起？
不知道，据说很有用。
#7 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 16日 10:34
由 forecasting
把证明转换成Lean语言的形式，现在不困难，尤其Tao发动一帮数学家做等式项目可以作为Lean语言的库。Lean说白了就是直觉逻辑的实现，换言之，就是把人做的证明转换成直觉逻辑的证明，现在有不少辅助工具，工作量不那么大。转换之后可以运行以检验原来的人工证明是否正确，前提是Lean语言的证明和人工证明等价，有时候转换会出问题，得小心检查或者debug。
#8 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 17日 12:19
由 wdong
#9 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 17日 16:14
由 forecasting
直觉如此，可得证明啊。
你在忙啥，还在做那agent？
#10 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 17日 20:00
由 heteroclinic
苏联笑话
废纸篓里三张废纸在白话
A : 我支持AI
B : 我反对AI
C : 我就是AI
#11 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 17日 21:34
由 TheMatrix
#12 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 18日 08:11
由 wdong
forecasting 写了： 2025年 6月 17日 16:14
直觉如此，可得证明啊。
你在忙啥，还在做那agent？
我现在主要在小红书发帖，看的人比较多。
#13 Re: 陶哲轩又送福利，数学分析1被改写成了Lean语言形式，想学AI数学证明的可以看看
发表于 ： 2025年 6月 18日 13:12
由 forecasting
wdong 写了： 2025年 6月 18日 08:11
我现在主要在小红书发帖，看的人比较多。
这是要做大V，会成为网红的。