46 lines
1.8 KiB
Markdown
46 lines
1.8 KiB
Markdown
---
|
||
title: "形式化定理证明（Formal Theorem Proving）"
|
||
created: 2026-07-03
|
||
updated: 2026-07-03
|
||
type: concept
|
||
tags: ["mathematics", "formal-verification", "theorem-proving", "lean"]
|
||
sources: ["arxiv:2606.03303"]
|
||
---
|
||
|
||
# 形式化定理证明
|
||
|
||
> 在机器可检查语言中编写证明，由严格内核（如 Lean、Isabelle、Coq）自动验证——解决自然语言证明不可靠的问题。
|
||
|
||
## 核心定义
|
||
|
||
**形式化定理证明** (Formal Theorem Proving, FTP / ATP) 是将数学证明用形式化语言编码，使得证明的正确性可以被机器自动验证。与自然语言（informal）数学推理不同，形式化证明提供了**保证的准确性**。
|
||
|
||
## 主要系统
|
||
|
||
| 系统 | 类型 | 特点 |
|
||
|------|------|------|
|
||
| Lean (Moura & Ullrich, 2021) | 依赖类型 | 活跃社区，mathlib4 库 |
|
||
| Isabelle (Nipkow et al., 2002) | 高阶逻辑 | 成熟的自动化工具 |
|
||
| Coq (Huet et al., 1997) | 构造演算 | 经典系统，丰富的库 |
|
||
| HOL Light (Harrison, 2009) | 高阶逻辑 | 轻量级内核 |
|
||
|
||
## 核心挑战
|
||
|
||
通用 LLM 在自然语言数学推理上表现强劲，但生成可验证的形式化证明仍然困难：
|
||
- 自然语言证明常含逻辑谬误和幻觉
|
||
- 验证瓶颈：Kepler 猜想经过 4 年同行评审才能声称「99% 确定」，最终需要十年形式化验证
|
||
- 非形式化到形式化的翻译鸿沟（[[autoformalization|自动形式化]]）
|
||
|
||
## 当前进展
|
||
|
||
- 专用证明器模型：AlphaProof、DeepSeek Prover V2、Seed Prover、Goedel Prover V2
|
||
- Agentic 框架：[[leap-agentic-atp|LEAP]]（仅用通用 LLM 达到 SOTA）、Hilbert、Aristotle
|
||
- 基准：MiniF2F、PutnamBench、[[lean-imo-bench|Lean-IMO-Bench]]
|
||
|
||
## 参考
|
||
|
||
- [[leap-agentic-atp|LEAP]]
|
||
- [[lean-proof-assistant|Lean 证明助手]]
|
||
- [[autoformalization|自动形式化]]
|
||
- [[lean-imo-bench|Lean-IMO-Bench]]
|