前言
写作【井蛙语海】的目的，是留存我学习语言（？）和语言学（？）的心得体会/读书笔记。间或记录学习过程中发掘的乐趣。我的目前的一个小目标是学会六门语言，即在已经学会的中文（(Emacs) Lisp），英语（Python）之外，努力掌握一定水平的法语（Rust）、日语（？？）、阿拉伯语（Erlang）和梵语（Lean）。并以这些语言为基础，学习语言学的相关知识，包括形态学、句法学（静态分析）、语义学（类型推断）、语用学（编译优化）。不过，虽然已经开始，但是作为数学系研究生的我实际上并没有太多的空余时间，所以这个专栏能走多远完全就随缘了。
Lean I-学习 Lean 的第一周（10-21~10-27）
（此乃谎言，事实上我之前在国庆的时候读了一遍 Theorem Proving in Lean 4，不过事实上里面的内容比较底层，对于数学证明来说有些过于复杂了。）
最近，有一个 Imperial College London 的本科学生来清华访问。刚好，他对于 Lean 比较感兴趣，所以和他聊了一下。他分享了 Kevin Buzzard 在 ICL 上课的材料 formalising-mathematics-2024 给我。这是写给数学家的 Lean 使用教程，比较全面地覆盖了各个数学分支在 Lean 中情况。避开了复杂的底层实现而集中在 Tactic 方法。在第一周的学习中，我完成了前六节的内容，包括逻辑、实数、函数、集合、群、序和格。
我们知道实数有多种定义的方法，包括公理定义、戴德金分割、有理数的柯西列的等价类等等。在 Lean 中，实数的实现采用的是有理数的柯西列的等价类的方法。这一方法在计算机中的公理化似乎比较简单。但是即使是要根据这一定义证明实数的性质就已经不是非常容易了。事实上，我最大的感受是 Lean 的推理水平忽高忽低。有的时候，不知道为什么用了 simp 就直接解决了所有的目标。但是有的时候要 rw 一些基础的等式都会失败。同时 Lean 的库虽然很大，而且提供了 exact?，apply? 等工具来帮助你查找需要的内容。但是我在做实数练习的时候还是因为不知道 lt_trichotomy 的存在而卡住。好在 Buzzard 好心地提供了所有练习的答案，所以如果不会至少还能看答案来解决。
在 Lean 中，集合也是一个有意思的概念。虽然在数学中，集合是最基础的概念，但是在 Lean 中类型（type）才是最基础的概念。所以所有的集合都有类型，这也就使得一些集合，比如 {{1}, 2, “cat”} 不能被简单地在 Lean 中被实现为一个集合。不过对于有编程语言学习经验的人来说这不算是一个特别大的困难。
除了实数和集合之外，在 Lean 中实现群、序、格更为简单。而在 Lean 中实现相关的证明也和手工证明的方法几乎没有差别。除了有的时候，Lean 会不按你想要的方式进行 rw，这时候必须需要使用一些迂回的方法，比如 have 一个新的定理等等。
总体来说使用 Lean 还是一件需要练习，而且花费时间的事情。虽然已经学习过相关的知识，但是通过将证明写成 Lean 能够理解的底层形式，还是需要我更好地理解证明。就目前我所学习的章节来看，将 Lean 引入数学本科的学习是完全有可能的，比如在抽象代数的学习中可以要求同学将证明题用 Lean 写出来。我不知道有没有学校进行过这样的尝试。当然，由于机器辅助证明还在快速发展中，不知道之后 Lean 会不会被更好的工具取代，所以让学生学习这些内容也存在过时的风险。
我不太喜欢 Lean 的一点在于它的使用基本上和 VSCode 是强绑定的关系。显然这是由于两个开发组都是微软主导的原因。以我浅薄的经验来看，如果不用 LSP server 提供的辅助信息，写证明的难度会大大增加。虽然官方也提供了 Emacs 的版本，但是 Emacs 的版本又必须依赖于 lsp-mode，而不能做到 LSP client independent。虽然，考虑到 Lean 的 LSP server 提供了一般 LSP 不会提供的复杂的信息来帮助证明的书写，这一点不是不能理解。但是 Emacs 的 lsp-mode 由于局限性存在性能问题，所以在 Emacs 上基本上 Lean 的使用非常不顺畅。当然，Lean 的 LSP 自身似乎也有一些内存和性能的问题，至少我在使用 VSCode 的时候，出现过 LSP 曾不知不觉占用了接近 2G 的内存，编辑器也出现了明显的卡顿的情况。不过，重启 Server 后问题得到了解决。