Vibe Mathing Router

识别当前数学研究瓶颈，只把任务交给一个 owner；不把整条研究链同时启动。

Position in the Method Map

路由器先问“规格和语义是否已经冻结”，再区分演绎证明、模型检查、抽象解释、SAT/SMT/符号推理（含符号执行）或精化/综合的验证范式。Lean 是依赖类型理论型演绎验证的主战场，不是整张形式化方法地图。完整的上位/二级地图见 FORMAL-METHODS-MAP.md。顶层编排语言见 RESEARCH-LIFECYCLE-MODEL-v0.1.md：路由器为 Step 选择 owner，不能把一次 Job 成功解释为数学结果。

When to Use This Skill

• 用户提出开放式数学问题，但尚未说明需要检索、推导、计算还是证明。
• 输入混合了论文、公式、猜想和代码，需要先决定当前最短验证路径。
• 用户问“下一步该做什么”或“该用哪个数学 skill”。

Not For / Boundaries

• 已明确要求符号计算、证明或 Lean 验证时，直接使用对应 owner。
• 不生成数学结论，不替代领域知识或机械验证。
• 不因输出文件类型选择路线；按当前阻塞选择。

Quick Reference

缺少问题边界/前人工作 -> math-discovery
公式对象、假设或近似不清 -> math-derivation
需要精确计算、数值实验、反例搜索 -> math-computation
需要定理证明、补步骤、攻击证明 -> math-proof
需要 Lean/内核级验证 -> math-formalization

路由输出必须包含：当前阶段、主 skill、选择理由、必需输入、停止条件、唯一下一步。

Examples

Example 1：开放问题

• 输入：“研究一下这个数列。”
• 动作：选择 math-discovery，先固定数列、已知项和检索边界。
• 验收：没有直接声称新定理，只给出可检索问题。

Example 2：明确恒等式

• 输入：“检查这个积分恒等式。”
• 动作：选择 math-computation。
• 验收：产出可重跑计算和适用条件，不标记为一般性证明。

Example 3：形式化请求

• 输入：“把这个证明写成 Lean。”
• 动作：选择 math-formalization 并先运行工具预检。
• 验收：Lean 缺失时状态为 blocked/calibration，不伪造 kernel-check。

References

• references/source-map.md：项目 owner 映射来源。
• references/pressure-tests.md：路由误触发压力场景。

Maintenance

• Sources：本项目 owner mapping 与供应链审计结果。
• Last updated：2026-09-07。
• Verification：python3 scripts/validate_project.py。