陶哲轩又送福利，数学分析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]

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