用途
Idea → Hypothesis → Proof Design（编排器）用于把一条原始研究想法，推进为一个形式化、可辩护的命题，并配上一套证明策略。它帮助用户锐化假设、隔离出必须成立的条件、精确陈述命题、勾勒证明，并在用户投入数周撰写完整论文之前先做审计。
该技能在多个单点技能之间进行路由——它本身不产出压力测试、证明草图或审计。
与同类技能的对比：
- learn-new-topic / deep-understanding：面向理解已有工作。而这里的对象是用户自己的想法，且尚不存在。
- gap-finder：从已有论文的弱点出发。用它来寻找想法来源；用本技能来发展你已经拥有的想法。
开始之前：捕获原始想法
只询问无法推断的信息。需要：
- 想法，用一句话表达——即使模糊也可以，将在第 1 阶段锐化。
- 设定——它涉及哪些数学/经验对象（它所处的形式体系）。
- “为真”意味着什么——用户追求的是定理、界、保证、不可能性结果，还是想要解释的经验规律。这决定了路径是证明设计还是实验设计。
如果用户实际想要的是经验验证而非证明，则改路由到 research-idea-stress-test → experiment-design，并明确说明。
流水线
按顺序执行。从想法当前所处的位置进入——已有清晰命题的用户可跳过第 1 阶段。
压力测试想法 → 提取必须成立的条件 → 陈述形式化命题 → 勾勒证明 → 审计与攻击 →（交接给写作）
第 1 阶段 — 压力测试想法 → research-idea-stress-test
交接出去，以暴露隐藏假设、虚假新颖性和混杂因素，并找到最廉价的测试来判断该想法是否值得形式化。不要为一个会被廉价攻击击倒的命题设计证明。 退出条件：想法在廉价反证下存活，且用户能分别陈述机制、命题与贡献。
第 2 阶段 — 提取必须成立的条件 → assumption-extractor
交接出去，列出命题所需的前提，把逻辑必要条件与便利条件分开。这些前提将成为定理的假设。 退出条件：存在显式的假设集合；用户知道命题缺了哪些前提就无法成立。
第 3 阶段 — 陈述形式化命题 → theorem-and-claim-audit
交接出去，把锐化后的想法加假设转化为精确量化的陈述，并检查命题是否被过度陈述、循环论证，或已被已知结果蕴含。 退出条件：存在一个带显式假设和量词的形式化命题，范围限定在实际可辩护的范围内。
第 4 阶段 — 勾勒证明 → proof-sketcher
交接出去，设计证明策略：高层论证、所需引理、证明技术，以及风险最高的步骤。可选地用 theory-to-toy-cases 在一个最小实例上验证该策略，再正式投入。 退出条件：存在带命名引理的证明骨架，并已识别出最薄弱环节。
第 5 阶段 — 审计与攻击 → counterexample-hunter（+ derivation-auditor）
交接出去，攻击命题与骨架：在假设边界处搜寻反例，并逐行审计任何具体推导步骤。这是过宽命题在到达审稿人之前被抓住的环节。 退出条件：对所述命题不存在存活的反例，且高风险推导步骤通过检查——或者命题已被收窄到两者都成立。
第 6 阶段 — 交接给写作
存活的命题加草图已准备好进行完整证明撰写和论文整合。路由到论文写作技能（method-section-writer、paper-argument-planner），如相关，再用 gap-finder 定位贡献。
路由规则
- 委托，不重复。每个阶段交接给一个单点技能；本文件负责排序与关卡。
- 按想法的成熟度进入。清晰命题跳过第 1–2 阶段；模糊直觉从第 1 阶段开始。
- 失败即循环。第 5 阶段出现反例，会把用户送回第 2 或第 3 阶段收窄命题——收窄是成功，不是失败。
- 证明，而非实验。如果“为真”意味着经验性，则这是错误的编排器——路由到实验设计流水线。
- 不要形式化已死的想法。如果第 1 阶段判定放弃或重构，就停在这里；不要为不值得的东西设计证明。
适用场景
- 已有数学或理论想法，想判断它是否值得形式化。
- 需要把模糊直觉锐化为可陈述、可辩护的命题。
- 需要搭建证明骨架并识别最薄弱环节。
- 希望在投入完整写作前先做反例攻击与推导审计。
限制
- 本技能是编排器，不直接产出压力测试、证明草图或审计结果。
- 若目标是经验验证而非证明，应改用实验设计流程。
- 具体收费、价格、平台支持等信息暂未提供。