tradecatlabs Math Discovery
把模糊兴趣变成可界定、可检索、可证伪的数学问题，并产出来源可追溯的证据图。
Position in the Method Map
本 skill 负责方法地图第一层的“规格与语义”前置：在选择 Lean、SMT、model checking 或 abstract interpretation 之前，先冻结对象、定义域、量词、来源和可接受结论。对应的机器边界是 ProblemContract；地图总览见 FORMAL-METHODS-MAP.md。
When to Use This Skill
- 需要查询某个定义、定理、证明技术或问题的前人工作。
- 需要从本地 admitted/candidate 问题语料发现研究方向，并判断来源成熟度或准入缺口。
- 需要建立关键词、别名、MSC/领域分类和检索式。
- 需要判断“是否已有类似结果”，或从冲突/空白形成候选猜想。
- 需要阅读论文并区分作者原始主张、证明依赖和当前综合判断。
Not For / Boundaries
- “没搜到”不等于“从未有人研究”。
- 搜索摘要不能替代读取定理陈述与证明正文。
- 不把博客、搜索摘要或模型总结当作原始证据。
- 不在没有证明/计算证据时把候选猜想提升为结果。
- CandidateObservation 是来源发现材料，
research_eligible=false；不得直接创建 Attempt，也不得把来源的answered/resolved/solved当作数学 Result。 - 默认只查询 admitted；只有用户明确需要扩展发现面时才使用
--collection candidates|all，并在输出中保留 collection、来源和许可边界。
Quick Reference
1. 固定对象、领域、问题和非目标。
2. 先查 `query_problem_library.py --collection admitted`；需要扩面时再显式查 candidates。
3. 建立术语：正式名、别名、旧名、符号、MSC、相邻领域术语。
4. 冻结检索式、来源、日期、语言和停止条件。
5. 优先原始论文、正式出版物、arXiv 原文和官方数据库记录。
6. 为每个来源记录稳定 ID、URL/DOI/arXiv ID、版本、raw locator 和证据位置。
7. 将关系标为 supports / contradicts / limits / extends / unknown；候选身份匹配只进入 review queue。
8. 输出已知事实、冲突、空白、候选猜想和下一步取证。
默认 provider 顺序：项目资源/MCP → SearXNG arxiv,semantic scholar,openalex,crossref →通用 Web。429/CAPTCHA 时记录失败并切换 provider；不无限重试。
Examples
Example 1：定理谱系
- 输入：“找 Szemerédi 正则性引理的主要变体。”
- 动作：冻结术语与范围，检索原论文和后续正式变体，构建依赖图。
- 验收：每项结论带稳定来源和定理位置；未读全文项标记未核验。
Example 2：序列查新
- 输入：一组整数项和生成规则。
- 动作：先确认规则与索引，再用 OEIS/论文检索，区分序列匹配与定理匹配。
- 验收：不会因 OEIS 命中直接声称生成机制相同。
Example 3：候选问题库选题
- 输入：“从新增问题库里找适合图论计算的开放问题。”
- 动作：显式查询 candidates，保留 source status、许可和 admission 状态；只生成待审 shortlist，不启动计算。
- 验收：每项均标为
research_eligible=false，唯一下一步是来源/陈述准入或 ProblemContract 冻结。
References
references/source-map.md：研究方法与检索供应链映射。references/pressure-tests.md：查新与摘要误用压力场景。
Maintenance
- Sources：
rw-research-skill、wentor-research-plugins、kdense-scientific-skills。 - Last updated：2026-08-13。
- Verification：供应链检查 + 搜索 provider smoke；外部数据库状态每次使用时重新核验。