5.5万字
机器如何读证明：Lean 与数学的形式化
数学形式化的百年理想如何在 Lean 中成为可运行的现实：从 de Bruijn 的证明检查器思想、Coq 与 Isabelle 的谱系，到 Lean 的依值类型内核与 tactic 元编程；并以陶哲轩《Analysis I》的 Lean 化为案例，逐条讲解皮亚诺公理如何被一个归纳定义整体吸收，兼述 AI 与形式化的交汇、限度与批评，以及完整的学习路径。
Read Analysis →(Σ :math)
数学 & 形式
数学理论、思想与形式化
约2千字
Lisp 宏：代码即数据的终极表达
从 McCarthy 的原始洞察出发，深入 Lisp 宏系统的核心机制——同像性使得代码与数据共享同一结构，从而赋予程序员改写语言本身的能力。本文通过渐进式示例、跨语言对比和形式系统的视角，揭示宏为何是元编程的终极形态。
Read Analysis →