Crab Research
研究首页/数学
旗舰研究计划 / 数学

Proof Engine

Crab Research 的旗舰数学研究计划。Proof Engine 通过精确的命题、可读的论证和可复现的证明证据，探索可靠的 AI 辅助数学研究。

组合数学 · 数论 · 几何17 篇数学结果论文 · 4 篇方法论论文

可信度与验证标准

形式化验证，是将定理和证明写成可由证明助手检查的精确形式。下面分别说明哪些检查已经完成、哪些前提仍然存在。

已完成内部审核的稿件（内部定稿）

已完成内部审核并公开，主要结论的完整形式化尚未确立；仍可能存在错误。

有外部定理前提的验证（Reference-Gated）

将部分引用定理明确列为前提，证明助手在这些前提成立的条件下检查其余推导；这些引用定理的证明尚未包含在发布包中。

仅依赖基础公理的验证（Kernel-Only）

证明助手检查包括引用结果在内的全部定理依赖，不额外假设任何尚未证明的定理。只允许下列作为推理起点的基础公理。我们还检查形式化与论文的对应关系；文字表述仍可能需要修订。

propext (命题外延性); Classical.choice (经典选择公理); Quot.sound (商类型健全性).

同行评审 · 已录用

经过独立同行评审，获期刊或同行评审会议录用，代表外部学术认可；录用与正式发表分别记录。

我们唯一接受的最终形式化标准是 Kernel-Only。Reference-Gated 的信任程度较低，仅在工程规模特别大时作为中间版本发布。同行评审不能消除尚未证明的定理前提。

展开查看验证方法与适用边界

精确的定理依赖

引用结果必须有精确的定理陈述、来源及对应的已检查形式化定理。可以复用 Lean/mathlib 中已有的内核检查证明。所有依赖最终只能归结到 propext、Classical.choice、Quot.sound；不接受额外定理公理、sorry 或未经内核检查的原生计算捷径。

Reference-Gated 版本必须公开引用关口清单：精确命题、假设与量词、来源位置、形式化前提，以及依赖它们的结论。达到 Kernel-Only 必须用已检查证明消除每个关口，并重新检查最终定理及其与论文的对应关系。

最终定理的公理报告说明证明实际依赖什么。仍须核对其命题是否对应预期的数学定理；仅有公理报告不能确立这种对应。

数学结果 17

SSRN 工作论文代表已经充分展开的研究，其中部分有意保留为独立工作论文。研究成熟度与发表状态分开记录。

17 项结果 · 按学术接受程度排序 · 记录更新 2026-09-06

初步工作论文 7展开论文收起论文

这些工作论文包括早期想法、初稿，以及有待进一步研究或验证的工作，作为进行中的研究公开。

我们认为，AI 时代数学的重要变化不只是成果数量的增长，更在于快速生成的内容凸显了既有数学体系中验证、解读、复用与维护之间缺失的工程层，并推动新的研究分工。AI 可以参与生成候选论证和探索证明路径，数学工程师等新兴角色将这些内容组织为可检查、可复现、可持续使用的成果，而数学家在提出有价值的问题、发现结构、创造概念以及解释和推广结果方面发挥核心作用。这些角色可以相互重叠，Proof Engine 正通过公开数学案例探索这种分工的基本可行性。 详细论证见我们的方法论论文。

方法论

Proof Engine 1.0 与 2.0

数学研究的两个互补层次：1.0 组织证明开发，2.0 治理数学探索，并可在其中使用 1.0。

Proof Engine 1.0

证明开发

组织精确命题、证据与依赖关系，明确保留待证义务，并将修正传递至相关论证。

阅读论文 · SSRN 7237460
首次公开发布
2026-07-29
最新公开修订
2026-08-31

Proof Engine 2.0

研究治理

治理数学探索中的问题、预期贡献和所需证据；自主执行保持在人类批准的范围内。

阅读论文 · Zenodo 工作论文
首次公开发布
2026-09-05
最新公开修订
2026-09-05

方法论论文 4

SSRN 工作论文代表已经充分展开的研究，其中部分有意保留为独立工作论文。研究成熟度与发表状态分开记录。

4 篇论文 · 按学术接受程度排序 · 记录更新 2026-09-06

返回研究首页