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

Lean 代码

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

改编自 google-deepmind/formal-conjectures 仓库的
FormalConjectures/Wikipedia/GoldbachConjecture.lean。改动：原文中该命题
出现在 `answer(sorry) ↔ ...` 的右侧；这里只登记命题本身，写成 `def`，因此文件中
不含 sorry。
-/
module

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

@[expose] public section

namespace Registry.Goldbach

/-- 表述 #20261014-02。

形状与 #20261014-01 相同，但“素数”取 Mathlib 中一般环论意义上的 `Prime`，
在 `ℕ` 上特化，与 formal-conjectures 的写法一致。 -/
def S20261014_02 : Prop :=
  ∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, Prime p ∧ 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 的源码片段，源文件 8ae01139b028。可人工修改。只解释定义和逐句翻译，不代表登记库判断，不涉及是否等价于原猜想。发现错误请提 PR 修改 Guides/Goldbach/S20261014_02.md。

定义解释

• Even：接受带加法运算类型中的一个元素（在此为自然数 n : ℕ），返回命题 Prop；表示存在某个元素 r 使得该元素等于 r + r。
• instCommMonoidWithZero：为自然数 ℕ 赋予带有零元的交换幺半群实例，使 ℕ 具备使用 Prime 谓词所需的代数结构。
• Prime：接受带有零元的交换幺半群中的一个元素（在此特化为自然数 p : ℕ），返回命题 Prop；表示该元素非零、不是可逆元，且对任意元素 a 和 b，只要能整除乘积 a * b，就必定整除 a 或整除 b。

逐句翻译

• 量词与前提：对任意自然数 n，如果 n 大于 2，并且 n 满足 Even；
• 结论：则存在自然数 p 和 q，满足 p 为素元（Prime）、q 为素元（Prime），且 n 等于 p + q。

问 Gemini

非正式复述

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

与 #20261014-01 相同，只是“素数”取一般环论意义上的 Prime（非零、非单位、整除乘积则必整除某一因子），作用于 ℕ。

声称的证明

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

＋ 声明证明了这条表述

暂无记录

外部链接

暂无记录

自己验证

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

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

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

编辑历史