anthropics/formal-math 来源：https://github.com/anthropics/formal-math # formal-math Anthropic 发布的经机器检查的 Lean 4 形式化成果。每个子目录都是一个独立的 Lake 项目，具有各自固定的工具链版本、README 和构建说明；请在子目录内进行构建。项目遵循 Palomar (https://palomar-registry.org/) 提交模板的布局（项目根目录下包含 Challenge.lean / Solution.lean / comparator.json / formalization.yaml），并以该子目录作为选定项目提交至 Palomar；Palomar 读取的许可证文件是本仓库根目录下的 LICENSE。 | 项目 | 命题 | Lean / Mathlib | |—|—|—| | zeta23/ | 黎曼 ζ 函数超过三分之二的零点是单零点且位于临界线上（Alpöge–Furman，arXiv:2608.13637） | leanprover/lean4:v4.33.0-rc2 / Mathlib v4.33.0-rc2 | | 3sum-apsp/ | 字长 RAM 程序可在 O(n^1.9992) 步内求解 3SUM，并在 O(n^2.99942) 步内求解 (min,+) 乘积和 APSP，所处理整数的大小为多项式量级；还逐项涵盖 Exact Triangle 和 Zero-Weight k-Clique 的界，以及论文中的其他结果（Alman–Vassilevska Williams，arXiv:2610.06783） | leanprover/lean4:v4.33.1 / Mathlib v4.33.1 | | eth/ | 存在一台确定性图灵机，对于每个具有 m ≥ 2 个子句、n ≥ 4 个变量且每个变量均有出现的 k-CNF，均可在 2^O(min{k^2 n log log n/√log n, km/√log m}) 步内计算其满足赋值的数量，从而推翻指数时间假设（Claude，文件夹内的论文） | leanprover/lean4:v4.33.1 / Mathlib v4.33.1 | ## CI 拉取请求和向 main 的推送会对文件发生更改的每个项目文件夹运行 .github/workflows/lean-projects.yml，且仅对这些文件夹运行；仅涉及 CI 配置或文档（.github/、本 README 等）的更改不会验证任何内容，所有项目的完整运行需从 Actions 选项卡手动启动（workflow_dispatch，projects = all）。如果设置了仓库或组织变量 LEAN_CI_RUNNER，verify 作业将在该变量指定的运行器标签上运行（例如 ubuntu-latest-16-cores 这样的 GitHub 大型运行器），否则在 ubuntu-latest 上运行。拉取请求的运行会复用该项目在相同工具链和清单下的上一次 Lake 构建（仅重新构建发生更改的模块）；合并到 main 和手动运行则从头构建。项目通过验证需要满足以下条件：在其固定版本的工具链上成功执行 lake build，且受信任的比较器命题文件（Challenge.lean、Challenge/.lean）之外不存在 sorry；同时，Palomar 注册表 (https://github.com/PalomarRegistry) 的验收检查——使用与工具链匹配的 lean4export、独立的 nanoda 内核和 landrun 沙箱，并采用注册表固定的工具版本运行 leanprover/comparator (https://github.com/leanprover/comparator)——对项目声明的每个比较器配置都输出 Your solution is okay!（.github/scripts/comparator-check.sh；在本地使用 cd && bash ../.github/scripts/comparator-check.sh 运行）。添加项目的方法：创建一个顶层目录，其中包含 lakefile.toml（或 lakefile.lean）、lean-toolchain、lake-manifest.json、一个仅依赖 Mathlib 且陈述主要定理的 Challenge 模块、一个基于库证明这些定理的 Solution 模块，以及至少一个比较器配置（与 lakefile 同级的 comparator.json，或 comparator/config*.json）；在上表中添加一行。 ## 许可证 Apache-2.0——参见 LICENSE。各个项目可能附带额外的 NOTICE 文件。