20260420:first commit

concepts/formal-verification.md

@@ -0,0 +1,54 @@
+---
+title: "Formal Verification (形式化验证)"
+created: 2025-04-15
+updated: 2025-04-15
+type: concept
+tags: [concept, mathematics, logic, ai-mathematics, verification]
+sources: [raw/papers/tao-ai-mathematical-methods-2026.md]
+---
+
+# Formal Verification (形式化验证)
+
+## 定义
+
+**Formal Verification** 是使用形式化方法（如一阶逻辑、集合论）来验证数学证明或计算机程序正确性的过程。
+
+## 历史背景
+
+数学传统上有客观的证明标准：
+- 从欧几里得到二十世纪初的基础
+- 尽管如此，人类数学家的论证通常不达到完美严格的理想
+- 错误是常见的，有些被修正，有些成为 "folklore"
+
+## 形式化验证的局限
+
+[[Terence Tao]] 在其论文中指出了形式化验证的两个关键局限：
+
+### 1. 翻译问题
+Formal verification only certifies that a formalized argument establishes a formal mathematical statement, but does not rule out errors in translation between the formal statement and the original intended statement.
+
+**Example** (陶哲轩的费马大定理例子)：
+- 费马大定理断言：对于 $n > 2$，方程 $a^n + b^n = c^n$ 没有自然数解
+- 隐含假设：自然数从 1 开始，而非 0
+- 如果 AI 错误地允许 $a, b, c$ 为 0，可能"证明"费马大定理是错误的！
+
+### 2. 无法捕捉 "Penumbra"
+即使形式化验证可以确保推理的正确性，它无法捕捉：
+- **Heuristics** 启发式 - 为什么这个方法有效
+- **Motivation** 动机 - 为什么要研究这个问题
+- **Context** 背景 - 如何广泛地理解这个结果
+- **Narrative** 叙事 - 证明的策略和构思
+
+## AI 时代的意义
+
+[[Terence Tao]] 认为：
+- AI 可以自动化形式化证明的生成
+- 但这可能产生 "odorless proofs"（无味证明）：技术上正确，但缺乏启发性
+- 人类数学家需要专注于那些不容易自动验证的方面
+
+## 关联页面
+
+- [[Mathematical methods and human thought in the age of AI]] - 详细讨论
+- [[Terence Tao]] - 该概念的主要阐述者
+- [[lean-mathlib]] - 论文提及的大型形式化数学库
+- [[smell-test]] - "气味测试"概念