数学家深挖 Lean 形式化证明：tactic 架构让证明难以像普通文本那样通读

burny_tech · x · 2026-09-08

一位数学家分享自己认真内化形式化数学语言的经历：为能像读本领域普通数学文本一样流畅理解形式化证明，他深入研究了 Lean（因流行度、类型论结构与 Mathlib 的表达能力），并借助 agent 自建了一个 Peano 算术的形式语言。

目前最大的障碍：许多 tactic 的架构使证明过程对读者很不友好，加上 Lean 的奇怪语法，读形式化证明时经常困惑；相比之下，他认为 Magma 把思想编码得更自然。这可能是他想改进的方向。