论Phaenarete Project的方法论基础与阶段性目标

写在前面

本文面向数学与计算机科学领域的研究者，旨在以技术语言阐明 Phaenarete Project 的方法论内核、工程架构与阶段性交付目标。我们将专注于三个问题：我们在做什么，为什么现在做，以及如何判断我们是否做成了。

我们不回避一个事实：黎曼猜想在本项目周期内被证明的概率极低。但我们同样不回避另一个事实：当前是构建"人机协同数学研究基础设施"的最佳窗口期，而解析数论——特别是围绕 $\zeta$ 函数零点分布的核心问题群——是检验这套基础设施的理想试金石。

选择最难的问题，不是因为我们自信能解决它，而是因为只有最难的问题才能暴露基础设施的全部缺陷。

一、问题的结构：RH 为什么难

初次接触黎曼猜想的研究者，容易将其理解为一个孤立命题。但一百六十六年的研究史表明，RH 实际上是一个问题网络的焦点，其困难源于多个深层结构的交汇。

解析维度。 $\zeta$ 函数零点的分布，本质上是关于 Dirichlet 级数的精细估计问题。这条线索从 Hardy1914 年证明临界线上有无穷多零点开始，经 Selberg 1940 年代证明正比例零点位于临界线上，到 Guth 与 Maynard 2024 年利用 decoupling 技术改进零密度估计，核心工具始终是调和分析与大值估计。每一步都耗费数十年，每一步都只融化了冰山的一角。

代数-几何维度。 Weil 1949 年对有限域上 $\zeta$ 函数的类比猜想，由 Deligne 1974 年最终证明。Gaitsgory 等人 2024 年发布的几何朗兰兹猜想证明（约 800 页，由 9 位数学家合作完成）进一步打通了自守形式与几何对象之间的通道。但从几何朗兰兹到数论朗兰兹，再到 RH，仍然存在从特征 0 到 $\mathbb{Z}$ 的巨大鸿沟。

谱维度。 1972 年，Montgomery 在普林斯顿的一次茶会上向 Dyson 描述了 $\zeta$ 函数零点间距的 pair correlation，Dyson 立即指出这与 GUE 随机矩阵的特征值间距相同。这一偶然发现开启了数论与随机矩阵理论之间长达半个世纪的对话。Connes 的非交换几何纲领试图为这种联系提供算子论框架，但至今未能给出完整的谱解释。

这三个维度之间存在深刻联系，但目前没有任何单一框架能够统一它们。这正是 RH 的核心困难，也是我们选择它作为基础设施压力测试的原因。

二、当前技术窗口的冷静评估

2.1 Guth-Maynard：方法论的示范

2024 年，Larry Guth 与 James Maynard 发表了关于 Dirichlet 多项式大值估计的新结果。他们将 Bourgain-Demeter 的 $\ell^2$ decoupling 定理引入解析数论，实现了对零密度估计的改进——这是自 Ingham 经典工作以来，该方向数十年未见的实质性进展。

这一进展的方法论意义大于数值意义。它证明了调和分析的现代工具可以有效作用于经典解析数论问题。但我们必须指出其局限：

decoupling 技术在 $\sigma \to 1/2^+$ 时存在本质的效率衰减，这不是技术细节，而是因为临界线附近零点分布的结构特征与 decoupling 所依赖的频率分离假设不兼容。
零密度估计的历史表明，每一次实质性改进都需要新的概念性输入，而非对已有方法的参数微调。

我们的定位：形式化其核心技术，理解其边界，而非期望通过算力堆砌实现线性外推。

2.2 张益唐的 Landau-Siegel 工作

2022 年，张益唐发布了关于 Landau-Siegel 零点问题的预印本，声称证明了 Dirichlet L-函数在 $s=1$ 附近不存在异常零点。如果成立，这将是该问题从指数级到多项式级的首次跨越。

需要诚实指出的是：截至本文撰写时，该论文的同行评审尚未完成，数学界对其完整性和正确性尚未达成共识。我们在项目中引用这一工作时，将严格区分"已发表的预印本"与"经同行评审确认的结果"。

即便该结果最终被确认，将其技术推广到复零点仍面临根本性障碍。张益唐的方法核心依赖于 $L(1, \chi)$ 的算术性质——特别是其与类数公式的联系——这些性质在 $\text{Re}(s) = 1/2$ 处没有直接类比。

我们的定位：形式化其论证中可独立验证的核心引理，精确刻画推广受阻的数学结构，将障碍本身作为知识资产记录。

2.3 Rodgers-Tao：de Bruijn-Newman 常数

2018-2020 年间，Brad Rodgers 与陶哲轩证明了 de Bruijn-Newman 常数 $\Lambda \geq 0$ 。这一结果将黎曼猜想等价于 $\Lambda = 0$ ，即一个精确的数值等式。

这一等价形式在概念上是优美的，但在技术上并未降低问题的难度——证明一个常数恰好等于零，通常比证明它的符号更困难。然而，它为数值探索提供了一个清晰的目标函数，这对 PrimeClaw 的 Explorer 智能体有潜在价值。

2.4 几何朗兰兹

2024 年，Dennis Gaitsgory 领导的团队（包括 Raskin、Rozenblyum 等 9 位数学家）发布了几何朗兰兹猜想的完整证明，总计约 800 页。这一工作打通了从 D-模到叠层的深层逻辑。

但我们不应高估其对 RH 的直接影响。几何朗兰兹处理的是特征 0 的函数域情形，而 RH 关心的是 $\mathbb{Z}$ 上的算术。从前者到后者的"算术化"是朗兰兹纲领中最困难的未解问题之一。我们将其视为 PrimeClaw 知识图谱中的重要节点，而非主攻方向。

三、AI 能力的诚实评估

3.1 已验证的能力边界

2024-2026 年间，AI 在数学推理领域取得了若干里程碑式进展。我们逐一评估其与本项目的相关性：

形式化证明搜索。 2024 年，DeepMind 的 AlphaProof 系统在国际数学奥林匹克（IMO 2024）中解决了 6 道题中的 4 道，达到银牌水平。其核心架构是将语言模型与 Lean 4 形式化验证结合，通过强化学习训练证明搜索策略。这证明了 AI 在竞赛级别的形式化推理上已达到可用水平。

但 IMO 题目与研究级数学之间存在本质差异：前者有明确的解，搜索空间有界；后者的解是否存在都是未知的，搜索空间无界。AlphaProof 的成功不能线性外推到 RH 级别的问题。

大模型的数学直觉。 陶哲轩在多个场合表示，他已将 AI 作为日常研究的辅助工具，用于快速检验猜想、生成反例、搜索文献中的相关结果。这种"AI 作为初级合作者"的模式，是我们 PrimeClaw 设计的直接灵感来源。

自动形式化。 将自然语言数学翻译为形式化证明的能力正在快速提升，但在前沿研究领域仍然不足。成熟理论（如本科级别的实分析）的自动形式化已基本可用；前沿技术（如 decoupling 估计的精细版本）的自动形式化仍需大量人工介入。

3.2 尚未验证的能力

概念创新。 没有证据表明 AI 能独立发明新的数学概念或框架。Guth-Maynard 将 decoupling 引入解析数论，这种跨领域的概念迁移仍是人类专属。
长程证明规划。 AI 在局部推理上表现优异，但在需要数百步、跨越多个子领域的长程规划上，尚无令人信服的案例。
失败诊断。 AI 可以尝试大量路径并报告失败，但提炼失败的结构性原因仍需人类介入。

3.3 我们的使用原则

基于上述评估，PrimeClaw 的设计哲学是：让 AI 做它擅长的事，让人做人擅长的事，用工程架构确保接口清晰。

人类负责：选择攻击路径、提供高维直觉、评估数学意义、诊断失败原因。

AI 负责：大规模引理搜索与生成、形式化翻译、参数空间扫描、已知技术的组合与变体生成、形式化验证。

工程架构负责：确保 AI 输出经过形式化验证才能进入知识库、通过置信度分级管理不确定性、记录所有探索路径的完整日志。

四、PrimeClaw 技术架构

4.1 四智能体协同

PrimeClaw 由四个专门化智能体组成：

Archivist（知识智能体）。 维护语义知识图谱，节点为数学概念、定理与技术，边为逻辑依赖、类比关系与已知障碍。输入源包括 arXiv 预印本、Mathlib 更新与项目内部探索日志。每日增量更新。

Explorer（探索智能体）。 基于蒙特卡洛树搜索（MCTS），在知识图谱约束下生成候选引理、猜想变体与类比映射。其输出被标记为置信度区间，而非二值判断。Explorer 被允许"犯错"——它的价值不在于每次输出都正确，而在于覆盖足够大的搜索空间。

Prover（证明智能体）。 接收经 Formalizer 翻译的 Lean 4 tactic 骨架，尝试填充sorry占位符生成完整证明。核心技术为微调的代码生成模型与 Lean 4 tactic 搜索的结合。

Sentinel（验证智能体）。 整个系统中唯一不使用概率模型的组件。它调用 Lean 4 内核类型检查器，对 Prover 的输出进行确定性验证。通过 Sentinel 的命题，其正确性由 Lean 4 的类型论保证，不依赖任何 AI 模型的置信度。

4.2 自动形式化中介层（Formalizer）

这是架构中最关键也最脆弱的环节。

Explorer 的输出通常是非形式化的（例如"对这个 Dirichlet 多项式做 Cauchy-Schwarz，然后用大筛法控制余项"）。直接交给 Prover 在 Lean 4 中实现，会因隐含假设暴露、"显然"步骤需要展开、类型不匹配等问题导致级联失败。

Formalizer 的职责是将这个翻译过程标准化：接收 Explorer 的伪代码输出，生成带sorry占位符的 Lean 4 tactic 骨架，再由 Prover 填充。

当前评估：在成熟理论上，翻译成功率已基本可用；在前沿研究上，成功率不足。这是项目前 6 个月的重点工程瓶颈。我们设计了人工回退机制——当自动翻译失败时，由 Lean 4 工程师手动完成关键步骤。

4.3 置信度有界类型

Turn-Lang 引入的置信度有界类型系统为 PrimeClaw 提供了管理不确定性的形式化框架：

Proven（置信度 = 1.0）。 经 Lean 4 内核验证。唯一可被下游证明无条件引用的级别。
Bounded（置信度 ∈ $[c_1, c_2]$ ）。 经数值验证或启发式检验但未形式化证明。可被引用，但引用方自动继承其置信度上界，确保不确定性的传播显式可追踪。
Speculative（置信度未定义）。 Explorer 的原始猜想。不可被任何证明引用，仅作为搜索方向提示。

工程实现依赖 Lean 4 的 tactic 框架。我们为 Bounded 类型设计了自定义oracle tactic，调用外部预言机并将结果包装为带置信度标记的项。编译器在类型检查时追踪置信度传播链，确保最终输出不包含任何未解决的 Bounded 依赖。

五、阶段性目标与交付物

第一阶段（第 1-6 个月）：基础建设

交付物：

Lean4 解析数论基础库 v0.1。 覆盖：Euler-Maclaurin 求和公式、Perron 公式及变体、大筛法不等式（Bombieri 型）、Dirichlet 多项式均值定理、 $\zeta$ 函数基本解析性质（函数方程、经典无零区域）。目标：不少于 200 个已验证引理。
PrimeClaw 原型 v0.1。 四智能体基本框架搭建完成。验收标准：在至少 3 个非平凡但已知的解析数论命题上，完成从自然语言输入到 Lean 4 证明输出的全流程。
知识图谱 v0.1。 覆盖解析数论核心文献（约 200 篇关键论文），节点包含形式化状态标记。

第二阶段（第 7-12 个月）：技术攻坚

交付物：

Guth-Maynard 核心估计的形式化。 策略：优先形式化论文的逻辑骨架（关键命题间的依赖关系），逐步填充技术细节。即使无法 100%完成，骨架本身将精确揭示当前形式化工具的瓶颈所在。
零密度估计参数探索报告。 利用 Explorer 在 Guth-Maynard 框架内系统性搜索参数改进。诚实预期：大概率不会找到实质性改进。但搜索过程将生成大量关于"为什么某些参数组合不工作"的形式化记录，以结构化数据公开发布。
Turn-Lang 编译器原型 v0.1。 支持从元语言到 CIC 的基本函子映射。验收标准：至少 10 个命题正确编译为 Lean 4 代码并通过类型检查。

第三阶段（第 13-18 个月）：拓展与整合

交付物：

Lean 4 形式化库 v1.0。 不少于 500 个已验证引理，提交 Mathlib 审核，MIT 许可证开源。
PrimeClaw v1.0。 完整系统，附技术文档与使用指南，开源发布。
谱维度探索报告。 在随机矩阵与谱理论方向生成可形式化验证的猜想变体。
Turn-Lang 编译器 v0.5。 支持置信度有界类型的运行时预言机。
《探索日志》全集。 所有路径（成功与失败）的完整记录，含自然语言描述、形式化状态、失败原因分析、相关文献引用。
终期评估报告。 对三大维度的探索进展进行诚实评估，明确哪些方向值得后续投入，哪些应当放弃。

六、团队与治理

6.1 核心团队

良之（项目负责人）。 整体架构设计、Turn-Lang 开发、资源协调。
Travor Liu（首席数学家）。 斯坦福大学博士生，数学方向判断、关键路径选择。
2-3 名全职形式化工程师（待招聘）。 将数学洞察转化为 Lean 代码，维护 Prover 与 Sentinel。

6.2 顾问团队与参与机制

我们不会假装院士们每周都在审阅代码。顾问的价值在于战略方向把关，而非日常技术参与。

刘建亚院士、孙斌勇院士。 月度书面咨询（不超过 5 页技术摘要），季度视频评估。
Yuri Matiyasevich 教授。 按需邮件咨询，针对 Diophantine 方向的具体技术问题。
张益唐教授。 荣誉顾问，参与主要体现在项目对其工作的形式化上。

6.3 质量控制

四层机制：

自动层： Sentinel 对所有形式化输出进行 Lean 4 类型检查，不可绕过。
工程层： 每周代码交叉审查。
数学层： Travor Liu 评估所有入库命题的数学意义。
战略层： 月度顾问反馈，季度全体评估。

七、风险登记簿

风险	概率	影响	缓解措施
形式化工作量超预期	高	第一阶段延迟	优先形式化逻辑骨架；与 Mathlib 社区合作
Formalizer 效率不足	中高	Explorer→Prover 管道堵塞	专项优化 + 人工回退机制
Turn-Lang 工程延迟	中	第二阶段交付缩水	与 PrimeClaw 主线解耦，确保独立运行
数学路径全部受阻	高	数学成果为零	交付目标已与"证明 RH"解耦；系统性记录失败本身是核心产出
关键人员或资金中断	低-中	项目缩减或终止	所有代码和数据从第一天起开源

关于"数学路径全部受阻"这一风险，我们需要特别坦诚：这是最可能的结果。RH 之所以悬而未决一百六十六年，不是因为前人不够聪明或工具不够先进，而是因为它可能需要尚未被发明的数学。我们的项目无法保证发明这种数学，但可以保证：如果它在我们的搜索空间内，PrimeClaw 有能力找到它；如果它不在，我们将精确记录搜索空间的边界，为后来者节省时间。

八、开放科学承诺

以下承诺不附加条件：

所有代码 MIT 许可证开源，托管于 GitHub。
所有形式化库提交 Mathlib 审核。
所有探索日志（含失败路径）以结构化数据公开发布。
季度进展报告在项目网站公开，包含成功与失败的诚实记录。
所有论文通过 arXiv 预印本发布，无访问限制。

在数学研究中，"我们试过了，走不通，原因如下"与"我们证明了"具有同等的知识价值。前者甚至可能更有价值，因为它帮助后来者避免重复劳动。

九、我们为什么仍然要做

读到这里的研究者可能会问：既然你们自己都承认大概率不会证明 RH，为什么还要做？

三个理由。

第一，基础设施的价值独立于 RH。解析数论的 Lean 4 形式化库目前几乎是空白。Mathlib 中与 $\zeta$ 函数直接相关的形式化内容极为有限。无论 RH 是否被触及，一个包含 500+核心引理的形式化库对整个数论社区都是实质性贡献。

第二，方法论的价值独立于 RH。PrimeClaw 的"四智能体协同 + 置信度分级 + 形式化验证"架构，如果在 RH 级别的压力测试下被证明可用，它可以迁移到任何数学研究问题上。我们在建造的不是一把只能开一扇门的钥匙，而是一套可以反复使用的锻造工具。

第三，失败的记录本身就是知识。数学史上，许多重大突破建立在前人系统性排除错误路径的基础上。Lakatos 在《证明与反驳》中指出，数学的进步不仅来自正确的证明，也来自对错误的深刻理解。我们承诺公开发布的《探索日志》——包含每条失败路径的形式化记录、失败原因的结构性分析、以及对搜索空间边界的精确刻画——将成为后续研究者的导航图。

这三个理由的共同指向是：Phaenarete Project 的成功标准不是"是否证明了 RH"，而是"是否为数学社区留下了可持续使用的资产"。

十、关于叙事的自我反思

我们意识到，本项目的早期宣传文本中使用了大量修辞性语言——肯尼迪登月演讲的引用、"历史奇点"的措辞、"思想的无限算力"等表述。这些语言在激发公众兴趣方面有其作用，但在学术语境中可能产生反效果。

数学家对"宣称攻克 RH"这类叙事天然警惕，这种警惕是健康的。历史上不乏声称证明 RH 的尝试，绝大多数在专家审查下迅速瓦解。我们不希望被归入这一类别。

因此，我们在此明确本项目的叙事边界：

我们不声称拥有证明 RH 的路径。我们拥有的是一套探索路径的系统性方法。
我们不声称 AI 能够独立解决 RH。我们声称的是，AI 可以显著加速形式化验证和引理搜索，从而提高人类数学家的探索效率。
我们不声称 18 个月后会有数学突破。我们声称的是，18 个月后会有一套可验证的基础设施交付物。

如果这些交付物最终促成了某个方向上的数学进展——哪怕只是一个微小的改进——那将是额外的收获，而非预设的承诺。

十一、对同行的邀请

Phaenarete Project 从第一天起就是一个开放项目。我们邀请以下方向的研究者参与：

解析数论方向。 如果你熟悉零密度估计、大值猜想、或 Dirichlet 多项式的精细结构，我们需要你的专业判断来校准 Explorer 的搜索方向。即使只是指出"这个方向不值得探索，因为……"，对我们也有巨大价值。

形式化数学方向。 如果你有 Lean 4（或其他证明助手）的开发经验，我们的形式化库需要贡献者。我们设立了悬赏池，对完成特定引理形式化的贡献者提供资金奖励。具体引理清单将在项目 GitHub 页面持续更新。

AI 与机器学习方向。 如果你在神经定理证明、自动形式化、或大模型数学推理方面有经验，PrimeClaw 的每个组件都有优化空间。Formalizer 的翻译效率是当前最紧迫的工程瓶颈。

数学哲学方向。 置信度有界类型系统引发了一系列认识论问题：一个依赖概率预言机的"证明"在什么意义上仍然是证明？形式化验证是否改变了数学真理的本质？我们欢迎这些方向的思考与批评。

所有贡献将在项目网站和相关论文中获得明确署名。我们相信，数学研究的未来属于开放协作，而非封闭竞争。

十二、技术附录：北极星命题的形式化

为确保 PrimeClaw 系统拥有统一的形式化目标，我们将黎曼猜想在 Lean 4 中写为一个命题。这段代码是项目的工程起点——我们把目标写清楚、写可检验，但不把它伪装成已完成的定理。

import Mathlib.Analysis.SpecialFunctions.Complex.Log
import Mathlib.Analysis.Complex.Basic

open Complex

/-!
# Phaenarete Project: Riemann Hypothesis — North Star Proposition

This file defines the Riemann Hypothesis as a formal Lean 4 proposition.
It serves as the project's engineering anchor: a machine-checkable goal
that all subsystems orient toward, without claiming any progress on its proof.

## Design Notes

- `riemannZeta` is declared as an axiom pending Mathlib's complete
 formalization of the analytic continuation of ζ(s).
- The statement restricts to the critical strip 0 < Re(s) < 1,
 excluding trivial zeros at negative even integers.
- This file compiles cleanly and contains zero `sorry`.
-/

/--
Placeholder for the Riemann zeta function, analytically continued
to the entire complex plane (except s = 1).

This axiom will be replaced by a concrete definition once Mathlib
provides a complete formalization of the meromorphic continuation.
-/
axiom riemannZeta : ℂ → ℂ

/--
**Riemann Hypothesis** (conjecture):

Every non-trivial zero of the Riemann zeta function lies on the
critical line Re(s) = 1/2. Equivalently, if ζ(s) = 0 and
0 < Re(s) < 1, then Re(s) = 1/2.
-/
def RiemannHypothesis : Prop :=
 ∀ s : ℂ, riemannZeta s = 0 →
 0 < s.re → s.re < 1 →
 s.re = 1 / 2

#check RiemannHypothesis

这个命题本身不包含任何数学内容——它只是一个类型签名。但它的存在确保了项目所有组件的输出最终指向同一个形式化目标。当 Mathlib 完成 $\zeta$ 函数解析延拓的形式化后，axiom riemannZeta将被替换为具体定义，届时这个命题将获得完整的数学语义。

结语

本文刻意回避了两种叙事：一种是"我们即将攻克 RH"的豪言壮语，另一种是"RH 不可能被证明"的虚无主义。我们选择的是第三种立场：承认问题的极端困难，同时相信系统性的努力——即使不能登顶——也能为后来者铺设道路。

一百六十六年前，黎曼在八页论文中写下那个猜想时，他大概没有想到它会成为数学史上最持久的悬案。我们同样无法预知，十八个月后我们会站在什么位置。但我们可以承诺的是：无论站在哪里，我们都会诚实地报告我们看到的风景——包括那些死胡同里的风景。

项目主页： Phaenarete Project 代码仓库： GitHub 联系方式： [email protected]

本文所有事实性陈述均经过公开来源核实。对于无法独立验证的信息（如尚未公开发表的系统或尚在同行评审中的论文），我们已在文中明确标注其状态。如发现任何事实错误，请通过上述邮箱联系我们，我们将在 24 小时内更正。