用途：把用户的数学陈述转成经过检查、且保持原意的 Lean 定理；继续已有的 Lean 证明项目；或审计某个 Lean 结果是否真正证明了原始命题。是否使用 Lean 取决于用户请求、是否在续写已有证明，或形式化能否解决核心命题中的具体不确定性；难度本身不构成形式化理由，普通推导可留在其他技能中。
主要能力与流程：核心工作流为原始陈述与 Lean 定义 → A 跨家族对抗式陈述对齐 → 证明义务、表示与引理接口 → Lean 实现与 B 关键论证对抗审查 → 接入真实输入并组装原定理 → 执行类型、定义与传递公理审计 → C 对最终导出结果做跨家族对抗审查 → 可复现交付与研究状态更新。大型新证明项目包含 A/B/C；续写时复用未变命题的已完成检查；小型常规形式化按实际命题比例检查。
使用方式：先读取权威陈述、现有 Lean 入口、工具链与 lockfile、最新进度记录，复用现有项目与文档命名，不重装工具、不改依赖、不另起框架。按请求范围执行实现、续写、审计或打包；审计只检查报告，不静默修复或弱化定理。实现时同时发展数学论证与 Lean 证明，搜索文献与库结果、探索替代路线、补齐缺失引理，并继续到接口与顶层组装，不停在首个编译成功处。
限制与注意：条件引理只是开发接口，临时 sorry 必须可见且不能进入最终目标；有限枚举只有在覆盖性、编码对应与验证过程都进入已证明依赖链时才构成证明；不得为让证明通过而静默引入公理或扩大信任基础。模型一致意见不是证明，同家族意见为暂定，跨家族意见只是额外审查证据。未读工件、未答问题、失败调用或空响应不构成实质审查结论。未解决的数学问题保持开放，不可用的审查保持待定；不得承诺任意开放问题可被形式化或解决。具体命令、安装方式与价格信息暂未提供。