表述 #20261014-01 · 哥德巴赫猜想

Lean 代码

/-
Formalia · 条目 #20261014-01
猜想：哥德巴赫猜想
内容许可：Apache-2.0（与原作相同）
原作版权：Copyright 2025 The Formal Conjectures Authors，Apache License 2.0

改编自 google-deepmind/formal-conjectures 仓库的
FormalConjectures/Wikipedia/GoldbachConjecture.lean。改动：把环论的 `Prime`
换成 `Nat.Prime`；原文中该命题出现在 `answer(sorry) ↔ ...` 的右侧，这里只登记
命题本身，写成 `def`，因此文件中不含 sorry。（最初误标为原创，2026-10-14 更正。）
-/
module

public import Mathlib.Data.Nat.Prime.Defs
public import Mathlib.Algebra.Group.Even

@[expose] public section

namespace Registry.Goldbach

/-- 表述 #20261014-01。

每个大于 2 的偶自然数都是两个素数之和，其中“素数”取 Mathlib 的 `Nat.Prime`。 -/
def S20261014_01 : Prop :=
  ∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q

end Registry.Goldbach

end

在浏览器里直接编译这段代码，不用安装任何东西。Lean 4 Web 使用最新版 Mathlib，和本站钉死的版本可能不同：那边报错不一定说明代码有问题，权威结果以下面的检查器报告为准。

检查器报告

定义链（直接依赖）

表述中直接出现的常量，以及定义它们的模块。到钉死版本的 Mathlib 中打开对应模块即可阅读其定义。

AI 导读

由 gemini-3.8-flash 于 2026-10-14 生成，依据 Mathlib v4.29.0 的源码片段，源文件 b5534de04f61。可人工修改。只解释定义和逐句翻译，不代表登记库判断，不涉及是否等价于原猜想。发现错误请提 PR 修改 Guides/Goldbach/S20261014_01.md。

定义解释

• Even：接受一个带有加法语义的类型中的元素（在本表述中为自然数 n : ℕ），返回一个命题 Prop，表示存在某个元素 r 满足 a = r + r。
• Nat.Prime：接受一个自然数 p : ℕ，返回一个命题 Prop，表示 p 是素数（定义为不可约数 Irreducible p，即大于等于 2 且只有 1 和自身两个约数的自然数）。

逐句翻译

对任意自然数 n：

若 n 大于 2，

且 n 是偶数，

则存在自然数 p 和 q，使得 p 是素数，且 q 是素数，且 n 等于 p + q。

问 Gemini

非正式复述

撰写者：提交者。这是撰写者对 Lean 代码的个人解读，不代表登记库的判断。

对任意自然数 n，若 n > 2 且 n 为偶数，则存在自然数 p 和 q，二者在 Nat.Prime 的意义下均为素数，且 n = p + q。

声称的证明

登记库只记录“谁声称证明了这个编号”，不托管证明，也不判断证明是否正确。

＋ 声明证明了这条表述

暂无记录

外部链接

暂无记录

自己验证

不想相信本站的检查结果？在自己电脑上用同样的版本重跑一遍：

git clone https://github.com/merethe-abeckett/formalia
cd formalia
git checkout 1fdef84bb2bb
lake exe cache get
lake build Conjectures.Goldbach.S20261014_01
lake exe check report.json Conjectures.Goldbach.S20261014_01
leanchecker Conjectures.Goldbach.S20261014_01

需要先安装 Lean（elan）。工具链 leanprover/lean4:v4.29.0 会按仓库里的 lean-toolchain 自动下载。第一次下载 Mathlib 缓存约 5 GB。

编辑历史