用途：将直觉性的数学想法整理为可检验的证明骨架，暴露结构、假设与未解决缺口，避免伪装成完整证明。
主要能力：精确陈述目标命题（含量化变量、定义域限制、渐近条件、概率限定与确切结论）；明确定义对象、记号与假设，并区分常设、临时与猜测性假设；把论证拆解为引理、命题、归约步骤与中间估计，形成依赖链；为每个阶段指定目标、候选技巧、依赖与可能薄弱点；显式标记缺口，区分已证步骤、启发式论证与猜想性推广；比较竞争性证明策略；最后给出最小下一步行动。
使用方式：按固定输出结构组织，包括目标命题、假设与定义、证明结构（逐引理列出目标、技巧、依赖、薄弱点）、缺口、替代策略与最小下一步。规则要求：优先显式假设而非隐含语境，宁可坦白不完整也不假装严谨，区分定理、启发式与猜想，避免叙述性填充与未定义记号，不跳过依赖链，不无理由称结果“显然”，不把多个逻辑步骤压缩成一句。
适用场景：数学或理论计算机科学研究中，在正式形式化之前梳理证明思路、检查假设充分性与依赖关系。
限制：资料未提供具体实现、安装方式、命令、平台支持、收费或效果信息，暂未提供。