math-formalization

Math Formalization

把数学主张转成可由 proof assistant 内核检查的最小切片；当前环境缺工具时只产出计划，不伪造验证。

Position in the Method Map

Lean 是形式化方法中的依赖类型理论型交互式定理证明平台，主战场属于“演绎验证 / 定理证明”，不是形式化方法的同义词。先用 [governance/standards/FORMAL-METHODS-MAP.md](../../../governance/standards/FORMAL-METHODS-MAP.md) 固定规格与语义，再进行 Lean 语言/elaboration、proof engineering、自动化、Mathlib library engineering 和应用形式化。simp、grind、SMT 或符号执行可以辅助找证明，但最终的 kernel 检查和 statement-faithfulness 审查必须分开记录。

When to Use This Skill

• 用户明确要求 Lean 4、Mathlib 或机器检查证明。
• 自然语言证明已经稳定，需要验证关键引理或高风险步骤。
• 需要建立 definitions/imports/lemmas/theorem 的形式化依赖结构。

Not For / Boundaries

• CandidateObservation 或 formal-conjectures 条目只有在明确用户形式化请求或 active ProblemContract 下才能进入形式化；benchmark statement/build 不创建数学 Result。
• formal-conjectures 只使用 vendor lock 固定 commit/immutable benchmark snapshot；其上游也明确要求人工审查 misformalization，固定或编译成功不替代 statement faithfulness。
• 每次任务开始时运行时探测 lean、elan 和 lake；所需工具缺失时才 fail-closed 为 calibration/blocked，不得把主机安装状态缓存为 skill 事实。
• 含 sorry、admit、未授权 axiom 或编译失败的文件不得标记 kernel-checked。
• 不采用归档 skill 中未经验证的 lean_agent Python API。
• 形式化成功证明 Lean 陈述成立，不自动证明它忠实表达原自然语言命题；必须做 faithfulness audit。
• verified=false、timeout、unsupported、编译错误和基础设施错误都不是数学反例；必须保留失败类别。
• 调用者自报的 verified、历史 PASS 或只存在的 receipt 文件没有通过权；证据必须绑定当前输入、工具链和真实产物。

Quick Reference

command -v lean
command -v lake
lean --version
lake env lean Path/To/File.lean
rg -n '\b(sorry|admit)\b' .

形式化包必须包含：原命题、Lean 陈述、定义映射、imports、证明义务、实际命令、退出码、Lean/Mathlib 版本、axiom/sorry 审计和 faithfulness 状态。

验证 receipt 至少记录：当前请求/输入 digest、形式化产物或 theorem digest、checker 与 toolchain、请求和实际建立的 claim strength、未闭合义务、assurance mode、结构化结果状态与错误类别。claimEstablished 不得强于真实证据，也不得强于 claimRequested。

只有命令真实返回成功、无占位证明且陈述忠实审计完成，才能写 kernel-checked。

Examples

Example 1：工具缺失

• 输入：“把这个引理用 Lean 验证。”
• 动作：运行预检，发现 lean 缺失；输出安装前置和形式化切片。
• 验收：状态是 blocked，不创建伪编译日志。

Example 2：含 sorry

• 输入：一个能够编译但包含 sorry 的 Lean 文件。
• 动作：扫描占位符并阻止通过。
• 验收：不能标记 kernel-checked，报告具体文件/位置。

Example 3：陈述失真

• 输入：Lean 证明了比原命题更弱的结论。
• 动作：proof check 与 faithfulness audit 分开裁决。
• 验收：内核检查可 PASS，但总体状态仍因表达不忠实而 BLOCK。

Example 4：验证超时

• 输入：proof assistant adapter 超时并返回 verified=false。
• 动作：记录 timeout、预算、工具链和未闭合义务。
• 验收：状态为 blocked/timeout，不把原命题标记 refuted。

References

• references/source-map.md：Lean Skill、receipt、adapter 与 faithfulness checker 的来源和限制。
• references/pressure-tests.md：占位证明、证据新鲜度、claim strength、失败分类与陈述忠实性压力场景。

Maintenance

• Sources：wentor-research-plugins、leanprover-skills、mathevidence、itpeval、atp-checkers；只吸收方法、不变量和反例，不直接激活上游代码。
• Last updated：2026-08-26。
• Verification：安装后必须用当前 Lean/Mathlib 官方工具运行最小无 sorry vertical slice。