tradecatlabs Math Formalization
把数学主张转成可由 proof assistant 内核检查的最小切片；当前环境缺工具时只产出计划，不伪造验证。
Position in the Method Map
Lean 是形式化方法中的依赖类型理论型交互式定理证明平台，主战场属于“演绎验证 / 定理证明”，不是形式化方法的同义词。先用 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_agentPython 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 官方工具运行最小无
sorryvertical slice。