AI辅助科学发现：从诺贝尔奖得主用Claude证明物理猜想看AI for Science新范式

📖读完本文你将获得：

• 理解AI for Science的范式转变：从数值计算到符号推理
• 掌握形式化证明（Formal Proof）的基本概念与工具链
• 了解大语言模型在科学证明中的三种协作模式
• 学会评估 AI 辅助证明的可靠性边界
• 预判 AI for Science 对科研流程的系统性影响

关键概念速览：

• AI for Science：AI 作为科学研究伙伴而非计算工具
• 形式化证明：用数学语言将证明过程转化为计算机可逐行验证的代码
• Lean 4：由微软研究院主导的交互式定理证明器，支持自然语言到形式化的转换
• 人机协作证明：科学家负责问题定义和策略，AI 负责细节推导和验证

AI 辅助科学发现（AI-Assisted Scientific Discovery）是指将人工智能系统作为科研过程中的认知伙伴，帮助科学家完成假设生成、理论推导、实验设计、数据分析等环节。

与传统计算工具的根本区别：

传统计算工具（如 Mathematica、MATLAB）执行的是确定性算法——给定输入，输出由算法严格决定。它们能计算微分方程的数值解、拟合实验数据、生成可视化图表，但不能「提出新的数学关系」或「发现证明思路」。

AI 辅助科学发现的核心在于创造性推理——AI 不仅能计算，还能提出新的猜想、尝试新的证明路径、发现隐藏的数学结构。这种能力来自大语言模型的模式识别和类比推理能力。

AI for Science 的三个发展阶段：

第一阶段（2016-2022）：AI 加速计算。 AlphaFold 预测蛋白质结构、DeepMind 控制核聚变等离子体。这个阶段 AI 的角色是「更快的计算器」——在已知框架内做更高效的事。

第二阶段（2023-2025）：AI 辅助假设生成。 AI 开始帮助科学家提出新的假设和猜想——从海量文献中发现潜在关联、生成可验证的科学假说、设计最优实验方案。

第三阶段（2026 至今）：AI 参与理论推导。 诺奖得主用 Claude 在 40 轮对话中完成 12 年物理猜想的证明，标志着 AI 进入了科学推理的深水区。AI 不再只是「算得更快」，而是「想得更深」。

大语言模型参与科学推理的底层能力来自三个方面：

第一，模式识别与类比迁移。LLM 在训练过程中接触过数百万篇学术论文，学习到了大量数学证明的「模式」——从归纳法的结构到群论的证明套路。当遇到新问题时，模型能识别出问题与已知模式之间的相似性，并将证明策略迁移过来。

第二，符号推理能力。现代 LLM（如 Claude 系列）在代码训练数据中学习了大量形式化系统的语法和语义——Lean、Coq、Isabelle 等定理证明器的语言。这使得模型能够输出形式化可验证的证明步骤，而非仅仅是自然语言描述。

第三，交互式修正能力。在 40 轮对话中，科学家可以对每一步推导进行质疑、要求修改、提供额外信息。这种迭代过程允许科学家引导 AI 沿着正确的证明路径前进，同时纠正 AI 的推理偏差。

LLM 辅助证明的局限性同样显著：

幻觉问题是最大风险。LLM 可能生成看似合理但实际错误的推导步骤。这就是为什么形式化验证不可或缺——每一步推导必须通过 Lean 4 等工具的逐行类型检查，否则证明无效。

上下文窗口限制意味着模型无法同时持有整个证明的所有细节。科学家需要将大问题分解为子问题，逐个与 AI 协作解决。

领域知识深度取决于训练数据。对于高度专业化的前沿领域（如某些弦论分支），模型可能缺乏足够的训练数据来提供有价值的推导。

AI 辅助科学证明需要三类工具的协同：

第一类：定理证明器（Theorem Prover）。 这是证明正确性的最终裁决者。主流工具包括：

• Lean 4：由 Leonardo de Moura（原微软研究院，现 AWS）主导开发的交互式定理证明器，语法接近函数式编程语言，拥有活跃的社区和越来越大的数学库（Mathlib）。2026 年已成为 AI 辅助证明的首选平台。
• Coq：历史最悠久的交互式定理证明器之一，在形式化验证和编程语言理论领域有深厚积累。
• Isabelle/HOL：适合高层数学推理，在工业界的形式化验证中有广泛应用。
• Proof 自动证明工具如 Vampire、E Prover：擅长一阶逻辑的自动化推理，但处理高级数学概念的能力有限。

第二类：形式化翻译器（Formalization Translator）。 将自然语言数学表述转化为定理证明器可理解的代码。这是 LLM 最擅长的环节——给定一个数学问题的自然语言描述，模型可以生成对应的 Lean 4 代码。

第三类：交互式协作界面。 科学家与 AI 之间的对话平台。可以是标准的 LLM 聊天界面（如 Claude Web），也可以是集成开发环境（如 VS Code + Lean 插件），甚至是可以直接执行和验证的 Notebook 环境。

完整工作流示例：

1. 科学家在 Lean 4 中定义定理陈述（theorem statement）
2. 科学家将问题描述发给 AI（Claude），请求证明思路
3. AI 生成自然语言的证明概要
4. 科学家根据概要，要求 AI 生成 Lean 4 形式的证明步骤
5. AI 输出 Lean 4 代码
6. 在 Lean 4 中运行类型检查
7. 如果通过 → 接受该步骤；如果失败 → 反馈错误给 AI，要求修正
8. 重复 3-7 直到整个证明通过验证

-- 定义一个简单的数学命题：偶数加偶数仍是偶数
def IsEven (n : Nat) : Prop :=
  ∃ k : Nat, n = 2 * k

theorem even_plus_even_is_even (a b : Nat)
    (ha : IsEven a) (hb : IsEven b) : IsEven (a + b) := by
  -- 展开 IsEven 的定义
  rcases ha with ⟨k₁, rfl⟩
  rcases hb with ⟨k₂, rfl⟩
  -- 现在需要证明 2*k₁ + 2*k₂ 是偶数
  -- 构造 witness: k₁ + k₂
  use k₁ + k₂
  -- 化简: 2*(k₁ + k₂) = 2*k₁ + 2*k₂
  ring

from dataclasses import dataclass
from typing import List, Optional
from enum import Enum

class VerificationStatus(Enum):
    PASSED = "passed"         # 形式化验证通过
    FAILED = "failed"         # 验证失败
    ADMITTED = "admitted"     # 有未证明的 admitted 步骤

@dataclass
class ProofStep:
    step_number: int
    natural_language: str      # 自然语言描述
    formal_code: str           # 形式化代码（如 Lean 4）
    status: VerificationStatus
    ai_confidence: float       # AI 自评置信度 0-1

@dataclass
class ProofReliabilityReport:
    total_steps: int
    passed_steps: int
    admitted_steps: int
    failed_steps: int
    peer_review_count: int     # 同行审查人数
    cross_validation_count: int # 交叉验证方法数
    fully_public: bool         # 对话记录是否公开
    
    @property
    def formal_score(self) -> int:
        if self.failed_steps > 0: return 0
        if self.admitted_steps > 0:
            return max(0, 40 - self.admitted_steps * 10)
        return 40
    
    @property
    def peer_score(self) -> int:
        if self.peer_review_count >= 3: return 25
        return self.peer_review_count * 8
    
    @property
    def cross_score(self) -> int:
        if self.cross_validation_count >= 2: return 20
        return self.cross_validation_count * 10
    
    @property
    def reproducibility_score(self) -> int:
        return 15 if self.fully_public else 0
    
    @property
    def total_score(self) -> int:
        return (self.formal_score + self.peer_score + 
                self.cross_score + self.reproducibility_score)
    
    @property
    def reliability_level(self) -> str:
        if self.total_score >= 85: return "高可靠性"
        if self.total_score >= 70: return "需补充验证"
        return "不建议发表"

def evaluate_proof(steps: List[ProofStep], 
                   peer_reviews: int,
                   cross_validations: int,
                   is_public: bool) -> ProofReliabilityReport:
    report = ProofReliabilityReport(
        total_steps=len(steps),
        passed_steps=sum(1 for s in steps if s.status == VerificationStatus.PASSED),
        admitted_steps=sum(1 for s in steps if s.status == VerificationStatus.ADMITTED),
        failed_steps=sum(1 for s in steps if s.status == VerificationStatus.FAILED),
        peer_review_count=peer_reviews,
        cross_validation_count=cross_validations,
        fully_public=is_public
    )
    return report

AI 辅助科学证明中的人机协作可以分为三种模式，代表了不同的分工深度：

模式一：AI 作为草稿纸（Scratchpad Mode）。 科学家主导整个证明过程，AI 仅用于完成繁琐的计算和代数变形。比如科学家说「帮我展开这个泰勒级数」，AI 执行并返回结果。这种模式风险最低，但 AI 的贡献也最小。

模式二：AI 作为合作者（Collaborator Mode）。 科学家和 AI 共同探索证明路径。科学家提出问题和验证标准，AI 提供候选推导步骤。这是诺奖得主与 Claude 协作所采用的模式。科学家负责「往哪个方向走」，AI 负责「这一步怎么走」。

模式三：AI 作为学生（Student Mode）。 科学家给出完整的证明概要，AI 负责填充所有技术细节并将其形式化。这种模式适合经验丰富的数学家——他们清楚证明的骨架，但不想在繁琐的细节上花费时间。

三种模式的对比：

合作者模式的最佳实践：

• 每步验证：AI 的每个推导步骤必须经过形式化验证或同行审查
• 主动质疑：科学家应主动质疑 AI 推导中的跳跃和隐含假设
• 记录决策：保留完整的对话记录，包括被拒绝的推导路径
• 分治策略：将大问题分解为独立可验证的子问题
• 冗余验证：关键步骤要求 AI 用不同方法重新推导

案例背景： ⚠️ 以下案例基于公开报道和行业传闻，具体细节尚未被官方来源完全确认。

据传，一位诺贝尔物理学奖得主（2025 年获奖）公开分享了他使用 Claude 完成一项持续 12 年的物理猜想证明的经历。整个证明过程仅用了 40 轮对话，引发了学术界和公众的广泛关注。

关键时间线：

该物理猜想最初提出于 2014 年，涉及一个描述特定量子系统中粒子行为的数学关系。12 年来，该猜想的证明一直是理论物理社区的开放问题。多位顶尖物理学家尝试过不同的方法，但均未能完成完整的严格证明。

AI 介入的过程：

第 1-5 轮：问题定义。 科学家将猜想的数学陈述用自然语言描述给 Claude，并提供了相关的物理背景和已有部分结果。Claude 确认理解了问题，并给出了初步的分析框架。

第 6-15 轮：策略探索。 Claude 尝试了多种证明路径。其中一些路径被科学家否决（基于物理直觉判断），另一些则被采纳并深入。这个阶段 Claude 的核心贡献是发现了已有文献中的一个被忽略的引理，并将其与猜想的关键部分建立了联系。

第 16-30 轮：推导执行。 Claude 沿着确定的证明路径进行详细推导。每一步推导都由科学家审查，关键步骤要求 Claude 用不同方法交叉验证。科学家在过程中多次指出 Claude 的推理跳跃，要求补充中间步骤。

第 31-40 轮：形式化与验证。 最终的证明被整理并尝试在形式化证明器中验证。Claude 协助将自然语言证明翻译为 Lean 4 代码。经过几轮修正（主要是类型注解和边界条件的补充），完整的证明通过了形式化验证。

这个案例的核心启示：

12 年未解决的猜想，在 AI 辅助下用 40 轮对话完成。这不是因为 AI「比人类聪明」，而是因为 AI 在信息检索（快速回顾大量数学文献）、模式匹配（发现被忽略的引理关联）、耐心迭代（不厌倦地反复修正推导）三个方面有显著优势。

但 AI 的成功离不开科学家的问题定义能力（知道问什么问题）、物理直觉（判断证明路径是否合理）、和验证标准（要求形式化验证而非接受自然语言论证）。

如何评估一个 AI 辅助产生的证明是否可靠？需要从四个维度进行判断：

第一维度：形式化验证通过率。 这是最基本的门槛。证明中的每一步推导是否通过了定理证明器的类型检查？是否有任何 admitted（承认但未证明）的步骤？一个完整的证明必须通过 100% 的形式化验证，不能有任何妥协。

第二维度：同行评审覆盖度。 即使形式化验证通过，证明的整体结构、前提假设和物理意义仍然需要人类专家的判断。建议至少邀请 2-3 位同领域专家对证明的每个主要部分进行独立审查。

第三维度：交叉验证一致性。 关键结论是否可以通过不同方法独立推导出来？比如，同一个引理是否可以用分析方法和代数方法分别证明？交叉验证是检测隐蔽错误的最后一道防线。

第四维度：可复现性。 完整的证明过程（包括与 AI 的对话记录、每个版本的推导、形式化代码）是否公开？其他研究者是否能够基于这些材料独立验证？科学发现的核心标准是可复现，AI 辅助证明也不例外。

可靠性评分表：

总分 ≥ 85 分可视为高可靠性证明，70-84 分需要补充验证，低于 70 分不建议公开发表。

AI 辅助科学证明不仅仅是工具层面的改进，它正在系统性地改变科学研究的各个环节：

研究选题的变化。 过去，科学家选择研究问题时需要考虑「这个问题是否在我有生之年可解」。AI 辅助证明大幅缩短了从猜想走向证明的时间，这意味着更多「大胆」的问题变得可行。研究者可以提出更具挑战性的问题，因为 AI 能分担大量推导工作。

论文写作方式的演变。 传统的数学和物理论文需要作者手工完成每一个推导步骤，读者也需要逐行验证。未来，论文可能会附带完整的形式化证明代码和 AI 协作记录，读者可以直接运行验证而非手动检查。

学术评审机制的革新。 审稿人不再需要逐行检查推导是否正确——形式化验证工具可以自动完成这一步。审稿人的精力可以集中在更重要的问题上：假设是否合理？方法是否创新？结论是否有意义？

人才培养模式的重构。 数学和物理教育可能需要重新思考：当 AI 能完成大部分推导工作时，学生的核心竞争力是什么？AI Master 认为，未来的科学人才需要更强的问题定义能力、跨领域连接能力、和批判性审查能力——这些正是 AI 目前无法替代的。

科学发现速度的跃升。 如果 AI 能将单个问题的证明时间缩短 10-50 倍，整个学科的知识积累速度将呈指数级增长。这可能带来科学发现的「寒武纪大爆发」——大量长期未解决的问题在短期内被集中攻克。

入门级：

• Lean 4 官方教程（lean-lang.org）：从零开始学习 Lean 4 语法和交互式证明
• Mathlib 文档（leanprover-community.github.io/mathlib4_docs）：Lean 4 的标准数学库
• 「Formalizing Mathematics」课程（Kevin Buzzard）：伦敦帝国理工学院的 Lean 4 数学形式化课程

进阶级：

• 「AI Theorem Proving」综述论文（arXiv, 2026）：系统回顾 AI 在自动定理证明中的最新进展
• Lean 4 + LLM 工作流指南（GitHub 开源项目）：展示如何将 Claude/GPT 集成到 Lean 4 证明流程中
• 「The Future of Mathematical Proof」演讲（Terence Tao, 2026）：菲尔兹奖得主对 AI 辅助证明的观点

前沿研究：

• MiniF2F 基准测试：标准化的形式化数学证明基准，用于评估 AI 证明能力
• ProofNet 数据集：从数学教材中提取的数千个形式化证明问题
• FunSearch 项目（DeepMind）：使用 LLM 在数学和计算机科学中发现新算法