这是 Lean II-学习 Lean 的第二周（10-28-11-03）。
这周我写完了 formalising-mathematics-2024 前 12 个 Section 的内容。然后尝试着做了一些之后的练习。从我个人的体验来看，前 12 个 Section（截至到 Filter）的内容是比较基础，简单的，而且证明的实现也比较简洁。但是从第 13 个 Section 开始，画风就不一样了。在一个子集 \(A \subset X\) 生成的 Measurable space 的可测集是 \(\{\emptyset, A, A^{c}, X\}\) 的证明中，即使是作为专家的 Buzzard 也必须进行繁琐的分类讨论。这种分类讨论在人类的证明中确实是不可缺少的，但是很多部分是简单而可以省略的，但是对于计算机就必须把它写出来。
在进行数论的几道练习的过程中，我又受到了 Int 和 Nat 之间的转换所带来的诸多问题。Lean4 虽然提供了一些方便的 tactics 比如 push_cast，norm_cast，zify 等来进行相关的操作，但是很多时候奇怪反而会让人抓狂。比如，我最开始尝试得到下面这个式子的证明，Lean4 却不能自动帮我完成这一点 \[n : \mathbb{N}, (1 + 2 * n + n^{2} - 2 * n):\mathbb{Z} = 1 + 2 * (n:\mathbb{Z})^{2} + n^{2} - 2 * n\] 后来我尝试进行下面这个式子的证明 \[n : \mathbb{N}, 1 + 2 * n + n^{2} - 2 * n = 1 + n^{2}\] 这对于人类来说是一个显然的事情，但是对于计算机来说，或者严格的理论来说，减法在自然数集上并不是良好定义的，所以 Lean4 不能自动帮你完成想要的简化。而且，你下面的式子也不被 Lean4 所承认。 \[n : \mathbb{N}, 1 + 2 * n + n^{2} - 2 * n = 1 + 2 * n - 2 * n + n^{2}\] 最后我发现我不应该在这里和减法过不去，应该使用加法的结合律，使用下面的等式 \[n : \mathbb{N}, 1 + 2 * n + n^{2} - 2 * n = 1 + n^{2} + 2 * n - 2 * n\] 然后 Lean4 就能进行进一步的简化了。这也可以看出，Lean4 的推理系统和人脑之间有着较大的差别。对于人脑来说显然等价的几种描述在 Lean4 中未必是等价的。同样的困难也出现在一些等式的化简过程中，比如在 Section 15 Sheet 4 中我们就需要进行带一个未知数的减法的化简。但是在 Lean4 中你必须明确告诉它目标，这一目标（式子简化的结果）却必须由手工计算得到，因为 Lean4 不是一个（好的）计算器。其次，需要将每一步的结果都清楚的写出来，很多时候，还必须告诉它（在哪里）进行什么样的变换，Lean4 才会承认你的证明。这样的过程是非常让人痛苦而心烦的，因为这一过程中没有任何数学的内容，甚至没有逻辑的内容，完全是一个非常初等的移项、合并等操作，但是 Lean4 却没有好的自动化手段。虽然 Lean4 提供了 exact?，apply?，aesop 等工具，但是这些工具效用相当有限，有的时候连一个简单的 rw 都不能帮我找到。从这些实践的经验来看，Lean 处理抽象的证明远远强于对于具体问题的解决，这也就大大提高了 Lean 的使用难度。
在 Section 19 中，Buzzard 提到 \(\text{FractionRing} \mathbb{Z} = \mathbb{Q}\) 类似的等式是不能在 Lean4 中被证明的，这是由于两边的类型不同。目前我尚不清楚这一问题对于证明形式化究竟有什么影响。但是这也是采用类型论的方法所必须支付的代价。对于数学家来说 Abuse of notation 是非常常用的手段，但是对于 Lean4，这种数学家所认为的等价性是不正确的。所以，对于数学家来说，类型转换的复杂性是 Lean4 难以应用的另一大痛点。
经过两周的学习，我对于 Lean4 的基本使用有了了解，但是由于对于 Mathlib4 库的了解还不够，以及对于 tactic 的使用还存在一些疑问的地方，所以证明往往写得曲折而冗长。看了 formalising-mathematics-2024 之后的内容，觉得有些过于困难，所以暂时不继续学习了。之后有空的时候再考虑要不要做一些代数几何相关的 formalizing 工作吧。