使用说明

一分钟看懂

猜想：一个用自然语言说的数学命题，比如“每个大于 2 的偶数都是两个素数之和”。每个猜想在 Formalia 有一个页面。
表述：把猜想写成 Lean 4 代码的一种写法，形如 def S20261014_01 : Prop := …。同一个猜想可以有很多种写法，每种写法一个永久编号，比如 #20261014-01。编号指向的代码永远不变。
声称的证明：某人或某个 AI 说“我证明了 #20261014-01”，并给出证明代码的链接。Formalia 只记下这句话和链接，不托管证明，也不认证。

所以一个猜想页就像维基百科的消歧义页：上面列出这个猜想的所有已知写法。哪一种写法忠实于原猜想，Formalia 不下结论，留给数学家判断。

怎样读一个表述页

基本信息：编号、提交者、日期、来源、许可，以及检查时用的 Lean 和 Mathlib 版本。
Lean 代码：登记的原文。冒号后面、:= 后面那部分就是命题本身。
检查器报告：机器自动检查的结果。能否编译、有没有 sorry（未完成的证明）、有没有 native_decide（绕过内核的计算），用到了哪些公理。只用 propext、Classical.choice、Quot.sound 三条标准公理才算干净。
定义链：表述里直接用到的每个名字来自哪里。绝大多数来自 Mathlib；如果表述自己定义了新概念，会单独标出“自定义定义”，这是最需要人仔细看的地方。
AI 导读：AI 对每个定义的解释和逐句翻译，可以在下面直接向它提问。它可能出错，只解释代码，不评价表述好坏。
非正式复述：提交者自己对代码的理解。
声称的证明：谁、何时、在哪里声称证明了这个编号。
编辑历史：这一条被谁改过什么。

不会 Lean 也能做的事

给表述补一段非正式复述或外部链接：点表述页上的“编辑本条信息”。
记录一条证明声明：看到有人宣布证明了某个编号，点“声明证明了这条表述”，填上声称方、日期和链接。
给猜想补中文名或参考资料：在猜想页点“编辑猜想信息”。
写一篇解读：这段 Lean 代码说了什么、和别的写法有什么不同、从证明里能读出什么。点表述页信息表里“解读”一行的“写一篇”，或在解读页点“写一篇解读”。解读是作者的个人观点，谁都可以修改。

登记一条新表述

在猜想页点“＋新增一条表述”，或在首页点“＋登记一条表述”（也可以顺便登记一个新猜想）。
在 import 里每行写一个 Mathlib 模块名，例如 Mathlib.Data.Nat.Prime.Defs。
在命题里只写命题本身，例如：∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ n = p + q。系统会自动包成 def S<编号> : Prop := …。
需要自己定义概念时，写在 辅助定义 里。
选来源类型和许可。改编别人的作品要填来源链接，并选与原作兼容的许可。
提交后会跳到状态页，几分钟内显示结果。

为了安全，代码只能用 Lean 的一个子集。下面这些会被拒绝：#eval 等 # 开头的命令、@[…] 属性、macro、syntax、set_option、IO、字符串、sorry、native_decide。import 只能来自 Mathlib 或 Batteries。

提交之后

机器检查格式；新增表述还要编译 Lean、运行检查器和独立复核，大约三到五分钟。
通过：直接写入，网站几分钟后更新。
没通过：状态页会写明原因，比如编译错误的那一行。改好后重新提交即可。
两个人同时改同一处时，后提交的人会看到“编辑冲突”，刷新后在最新内容上重做。

不接受什么

等价性争论：“这条不算真正的哥德巴赫猜想”不是修改或删除的理由。觉得现有写法都不对，就登记一种新写法。
证明代码：请放在你自己的仓库里，这里只放链接。
评价性文字：条目里只写事实。

常见问题

为什么不能直接改别人的 Lean 代码？ 因为“某人证明了 #20261014-01”这句话必须永远指向同一段代码。要改代码，就登记一条新表述，旧编号保留。

我的提交为什么没通过？ 打开状态页看原因。最常见的是 Mathlib 里的名字写错，或用了上面列出的被禁写法。

可以在自己电脑上检查吗？ 可以。每个表述页底部有“自己验证”的命令，也可以点“在 Lean 4 Web 中打开”在浏览器里试编译。

中国大陆能用吗？ 网站和编辑表单都不依赖 GitHub 账号。GitHub 页面打不开也没关系，状态页会显示同样的结果。

我的 IP 会被公开吗？ 不会。公开的只有由 IP 派生的匿名编号，详见隐私与编辑规则。