GitHub · 去对齐工具与仓库·· 4 天前精选AI 评分66
MathProof Skill v0.2.0 发布：用 Lean 4 对抗式审计 AI 数学证明
Ztang-Yit-Xiaang/mathproof-skill
来源与原文
GitHub · 去对齐工具与仓库
发布时间：（北京时间）
阅读原始来源 · github.com ↗完整链接与内容说明
https://github.com/Ztang-Yit-Xiaang/mathproof-skill
本站目前仅有 AI 导读与摘要，未展示原文正文；技术细节、代码和完整结论请查看原始来源。
AI 导读
作者发布 MathProof Skill v0.2.0，一个让 AI 在接受数学证明前先尝试推翻它的技能，核心流程为 Claim、假设、对抗审计、依赖图、证明、二次审计、Lean 校验。该技能用 Lean 4 + Mathlib 形式化命题并运行检查器，拒绝 sorry、自定义公理和内核绕过，仅通过检查的结果才算机器校验；仓库含六个带真实运行输出的评测案例（含梯度下降 O(1/k) 速率证明）、四种模式（PROVE/AUDIT/EXPLAIN/RESEARCH）和五种判定结果，可通过 /plugin install mathproof-skill 安装到 Claude Code，MIT 许可。
推荐理由
作者给出 Lean 4 + Mathlib 的机器校验流程和六个带真实运行输出的评测案例，读者可以照着复现这套对抗式证明审计方法。
来源：GitHub · 去对齐工具与仓库 · github.com