Lean是一种主要用于数学的编程语言，旨在将数学形式化为代码，使数学家能够将数学分解为结构、定理和证明，并在GitHub上共享。通过Lean，人类的大部分数学知识可能最终会以静态检查、可验证和可组合的代码形式存在。使用Lean时，数学定理的声明和证明过程类似于编程中的函数定义，展示了数学与编程的紧密联系。

文章主要内容：

作者最近在大量使用Lean，这是一种主要用于数学家的编程语言，旨在将数学形式化。Lean允许数学家将数学视为代码，将其分解为结构、定理和证明，并可以在GitHub上共享这些内容。最终目标是让人类的数学知识以代码的形式存在，具备静态检查、可验证和可组合的特性。

Lean的使用体验：

作者通过一个简单的例子展示了Lean的使用方式。例如，证明2 = 2的定理：

lean theorem two_eq_two : 2 = 2 := by rfl

这里的rfl表示“自反性”，即“一个事物等于其自身”。通过这种方式，Lean允许用户逐步构建和验证数学证明。

数学的“幽灵”：

作者进一步探讨了如何在Lean中处理不寻常的数学命题，例如2 = 3。通过引入一个公理（axiom），可以“证明”这种不成立的等式：

lean axiom math_is_haunted : 2 = 3

借助这个公理，甚至可以“证明”2 + 2 = 6。然而，这种公理会导致逻辑矛盾，进而使得任何命题都可以被“证明”。作者指出，这与20世纪初集合论中的罗素悖论类似，当时数学家们不得不重新选择公理来修复这一问题。

费马大定理的证明：

作者提到，费马大定理（Fermat's Last Theorem）的证明在1994年完成，但至今仍在努力将其形式化到Lean中。这一过程预计需要多年时间，因为需要建立大量的数学结构和定理。

下一步：

作者建议对Lean感兴趣的读者可以从自然数游戏（Natural Numbers Game）开始，这是一个轻松有趣的入门方式。此外，Mathematics in Lean和Tao的《分析》的Lean版本也是很好的学习资源。

总结：

Lean作为一种形式化数学的工具，允许用户通过代码的方式构建和验证数学证明。虽然它可以帮助数学家处理复杂的逻辑结构，但选择正确的公理至关重要，否则可能导致逻辑矛盾。Lean的学习过程既像编程，又像数学推理，适合那些对数学和编程都感兴趣的人。

评论内容总结：

1. Lean 学习难度与语义模糊性

   • 主要观点：Lean 的战术（如 rfl）语义不明确，教程未能充分解释，导致学习难度较大。
   • 关键引用：
     • "tactics - like rfl in the example - are overloaded, and their full semantics not completely explained/understandable from the tutorials"
     • "the rewrite (rw) tactic syntax doesn't feel natural either"

2. Lean 的验证模式与证明可信度

   • 主要观点：Lean 是否具备验证模式，确保证明不依赖 sorry 或额外公理。
   • 关键引用：
     • "Does Lean have some sort of verification mode for untrusted proofs that guarantees that a given proof certainly does not use any 'sorry'?"

3. 形式化定理与自然语言表述的匹配问题

   • 主要观点：Lean 无法确保形式化定理与自然语言表述完全一致，尤其是在复杂定理中。
   • 关键引用：
     • "Lean doesn't solve the problem of verifying that a formal theorem actually states what we think it states rather than something else"
     • "in other cases it might be much harder to verify that a formal statement actually matches the intuitive informal statement we want"

4. Lean 在非虚构写作中的应用

   • 主要观点：Lean 可用于重写新闻或非虚构文章，将陈述视为需要证明的定理，并通过引用进行验证。
   • 关键引用：
     • "to rewrite news and other non-fiction articles, treating statements as theorems that need to be proven"
     • "Proofs could include citations, and could be compound things like 'this is a fact if three of my approved sources asserted it as a fact'"

5. 数学证明的逻辑构建与游戏化

   • 主要观点：数学证明的逻辑构建过程具有吸引力，可将其游戏化，激发兴趣。
   • 关键引用：
     • "Can someone please turn this into a Zachtronics style game?!"
     • "The sheer thrill of adding to that dictionary of proofs?"

6. 数学证明的标准库与共享

   • 主要观点：是否存在标准库或存储库，供人们添加和共享现有数学证明。
   • 关键引用：
     • "Is there a standard library/repository of all existing mathematical proofs one can add to?"