关于 Formalia

Formalia 是什么

Formalia 是一个中立的目录，收录数学猜想的 Lean 4 形式化表述。它只记录事实：每条表述的代码、它依赖的定义、谁提交的、机器检查的结果，以及谁声称证明了它。它不判断一条表述是否等价于原猜想。

原则

• 只列出，不判断。 等价性由数学家讨论，不在本站作结论。
• 编号永久。 一个编号永远指向同一段代码。
• 机器把关。 收录与否只看自动检查：能编译，没有 sorry、native_decide，只用标准公理，并经独立内核复核。
• 谁都可以编辑。 不需要注册，不需要 GitHub 账号；每次编辑都有记录，可以回退。
• 公开透明。 代码、数据、编辑历史全部公开在 GitHub。

许可

代码 Apache-2.0。条目内容按各条目声明的许可发布，未声明时默认 CC-BY-4.0；改编别人的作品沿用原作许可。

联系

• 仓库：github.com/merethe-abeckett/formalia
• 邮箱和作者的话：见联系作者

作者的话

我觉得我们可以建立一个仓库，人类社区贡献者只负责转写原猜想命题至证明语言（现阶段先做 Lean 4，以后不一定非得是 Lean 4，任何证明语言都可以），比如 Hodge 猜想可以转写成 Lean 4 的 #20261010 或 #20261004 等数字编号的表述，然后 LLM（人类也可以，当然）只负责提供能证明或证否这些命题的 Lean 代码，放在自己的仓库里，到这里登记一句“我证明了 #某编号”，由其他 AI 或人类贡献者跑 Lean 来独立验证。这样一来，数学家可以选择认可或者不认可这些原猜想的 Lean 4 表述是否等价于原猜想，且任何人和公司都可以快速发布并快速被核查。而对未来数学家可以干什么我其实也有回答，就是做数学的解释学，和生物分类学家看 iNat 来鉴定和分类类似，一个是认领这些证明，一个则是从这些证明语言（不管是 LLM 还是人类写的）里面挖掘东西。数学博物学万岁!

上面是愿景，下面是本仓库现阶段的规则。两者有一处要先说清：本仓库本身不审稿，也不认证。模型在这里只做巡查，查 Lean 层面的问题；Lean 内核和 CI 查证明对不对；“表述等不等价于原猜想”谁都不查，留给数学家线下讨论。至于模型审稿、人类做解释学，那是下一阶段在别处发生的事，本仓库只负责把编号、表述、声明列清楚，让那些事有据可依。

本仓库强烈建议用户用中文普通话和各地中文方言完成对贡献的说明部分的补全，包括来源备注、非正式复述、PR 和议题里的说明。Lean 代码、JSON 字段名和 Mathlib 名称保持原样。