Meme of LinOnetwo

theorem_proving_in_lean4

natural_number_game

学习目标

1. 调研能否表达因果论里的定理和逻辑，比用 LaTex 做笔记更有意思
   1. 见下面友好的命名，至少这点让我更容易记住定理
   2. 可表示概率论概念 mathlib-overview#probability-theory
2. 调研能否用于替代机器学习里的LaTex公式做笔记
3. 学习和比较编程语言中的 Dependent Type
4. 用它验证和搞清楚量化交易中用到的公式

友好的命名

我们称这个定理为add_zero 。更准确地说，add_zero 是定理证明的名称。注意这个证明的名称。数学家有时称之为“引理2.1”或者“假设 P6”之类的。但是计算机科学家称之为 add_zero ，因为它告诉你“加零”的答案是什么。这名字比“引理2.1”好多了。更好的是，我们使用重写策略的时候可以直接用 add_zero 这个名字，更容易想起来。

教程世界 lv4

学习方法

翻 mathlib，从大学学过还记得的定理看起，自己整理到一个wiki里，让AI：给出其LaTex版本和现实意义，并设计两道Lean4表示的例题

用$:/plugins/tidme/fsrs4tw间隔重复然后继续学习相关定理。

实分析游戏

数学分析课本

原因

从高中开始我就觉得写数学题很烦，因为要写一大堆的字。我讨厌用手写字，更喜欢打字，所以到了大学之后我尝试用 LaTeX 记笔记，但感觉打起来很累，而且输入进去之后它并不能自动解题，不像写代码一样输入了就会自己动起来。

那时候我了解到了 Coq，但它不是很好表示大部分能用 LaTex 轻易输入的概念。后来开始看因果论之后，我又在一个编程语言理论的学习群里问了一下有什么能表示概率论的数学语言，当时有人推荐了 Lean，但当时没搞清楚它是否真的能表示概率论相关的定理，就只加入了收藏夹没继续学。

后来看到陶哲轩的 Lean4 搭配 ChatGPT 自动证明定理很方便的新闻，就又激发了学习兴趣。

读到2025年你的数学研究或学习有什么收获和感悟？ - bigpunch的回答 - 知乎又激发了学习兴趣。