用途：为 ML/AI 理论撰写严谨的数学证明，适用于被要求证明定理、引理、命题或推论，或补全缺失证明步骤的场景。
主要能力：产出三类结果之一——原命题的完整证明、修正命题及其证明、或说明命题当前无法成立的阻塞报告。工作流程包括收集证明上下文、规范化命题、可行性分级（PROVABLE AS STATED / PROVABLE AFTER WEAKENING / NOT CURRENTLY JUSTIFIED）、构建依赖图、撰写证明文档、最终校验。要求不使用“显然”“同理”等掩盖证明缺口，需定义符号、检查量词顺序、处理边界情形，并用 $...$ 与 $$...$$ 书写数学。
使用方式：默认输出到项目根目录的 PROOF_PACKAGE.md，除非用户指定文件路径。文档结构含 Claim、Status、Assumptions、Notation、Proof Strategy、Dependency Map、Proof、Corrections or Missing Assumptions、Open Risks。用户请求 Lean 时或形式化有助于验证时，可调用 /lean-formalize，但普通证明撰写不需要 Lean。
限制：不得编造证明步骤，优先弱化命题而非过度声称；若命题为假需明确说明并给出反例或修正；不确定之处须在 Open Risks 中标注。具体安装命令、收费与平台信息暂未提供。