Lean 表述登记库
一个中立的目录，收录数学猜想的 Lean 4 形式化表述。每个猜想有一个消歧义页，列出已登记的各条表述；每条表述的页面记录 Lean 代码、钉死版本的定义链、来源、自动检查结果，以及声称证明了它的证明。仅此而已。
工具链 leanprover/lean4:v4.29.0 · Mathlib 8a178386ffc0f5fef0b77738bb5449d50efeea95 · 最近一次检查： 全部条目通过
猜想列表
| 猜想 | 已登记表述数 |
|---|---|
| 哥德巴赫猜想 Goldbach's conjecture | 2 |
谁都可以编辑
和维基百科一样，不需要注册，也不需要 GitHub 账号。每个页面上都有编辑按钮。提交后机器会自动检查：Lean 代码要能编译，不能有 sorry、native_decide 或非标准公理，并经 lean4checker 独立复核。检查通过就直接写入，网站几分钟后更新；每一次编辑都留有记录，可以回退。是否等价于原猜想不在检查范围内，留给数学家讨论。
隐私与编辑规则 · 熟悉 GitHub 的人也可以直接提交 Pull Request，见 README。