tradecatlabs Math Computation
用成熟计算库生成可重跑证据；计算用于发现、反驳和核对，不越权成为一般性证明。
Position in the Method Map
本 skill 覆盖形式化方法地图中的“SAT/SMT、符号执行和决策过程”横向自动化，以及有限的数值/符号实验；它不替代规格与语义、演绎证明、模型检查或抽象解释。需要 Lean proof term 和 kernel 检查时转交 math-formalization，需要精确定义和来源时先转交 math-discovery。完整地图见 FORMAL-METHODS-MAP.md。
When to Use This Skill
- 需要精确化简、求解、积分、极限、级数、矩阵或多项式计算。
- 需要高精度数值交叉检查、参数扫描或有限范围反例搜索。
- 需要识别整数序列、测试猜想小规模实例或生成图表数据。
- 需要为数论、有限代数、图论、SAT/SMT、代数几何或 PDE 实验选择成熟工具。
Not For / Boundaries
- 只有明确用户计算请求或 active ProblemContract 才能启动研究计算；CandidateObservation 必须先回到
math-discovery完成准入。 - 工具只有达到
smoke_checked才可生成计算证据，只有独立 verifier adapter 达到verifier_admitted才可作为验证器；survey 文档和固定源码不算运行能力。 - 浮点相等不是数学恒等；优先 exact arithmetic。
- SymPy 返回结果可能带分支、条件或未求值对象，必须检查。
- 有限枚举“未发现反例”不证明全称命题。
- 大规模矩阵/扫描必须先估算复杂度、内存和停止条件；任何计算、外部命令、solver、枚举或 Lean/CAS 子任务必须有 wall-time、内存/线程/输出预算、可登记的终止回执，禁止裸
solve()或无 timeout heredoc。
GPU 可行性预检（强制）
任何计算动手前，先运行 python3 scripts/compute_plan.py --kind <类型> --n <规模> --dtype <精度>，批量搜索还必须提供 --ops-per-sample 或 --flops；按输出 route 选择 CPU 或 GPU，并把路由决策与原因写入执行记录：
| 工具族 | 解释与说明 |
|---|---|
symbolic 与 mpmath |
固定走 CPU；精确或任意精度计算没有本项目 GPU route。 |
small-numeric |
固定走 CPU；单次小规模任务的 GPU 无收益。 |
dense-numeric |
只有规模/运算量达阈值、精度为 f32/f64 且 GPU 可用时才考虑 GPU；否则回退 CPU。 |
batch-search |
只有运算量达阈值且 GPU 可用时才考虑 GPU；GPU 只做粗筛，精确复核回 CPU。 |
- GPU 不可用、GPU 队列忙或可用内存不足时回退 CPU，并在执行记录标注原因；
COMPUTE_FORCE_CPU=1可强制走 CPU，节点预算由COMPUTE_MEMORY_BUDGET_GB/COMPUTE_MEMORY_HEADROOM_GB/COMPUTE_THREADS_MAX运行时注入。 - GPU 只做粗筛/预筛；结果只能作为
numeric-check支持，不得提升证据等级；候选必须回 CPU 用 SymPy/mpmath/FP64 精确复核。 - 多 Agent 并行时遵守项目 AGENTS.md「计算资源与 GPU 路由（强制）」：线程上限、GPU 全局串行锁、内存水位门禁。
Quick Reference
先按问题域运行能力探针；不得只凭包名、PATH 或 Agent 自报认定工具可用：
python3 scripts/check_math_tools.py --profile <profile> --strict
profile 与具体工具入口见 references/tool-catalog.md。项目 .venv、系统 Python、Sage 和 Lean 是独立运行时，禁止跨运行时猜测 import。
import sympy as sp
x = sp.symbols("x", real=True)
delta = sp.simplify(lhs - rhs)
status = "symbolically-checked" if delta == 0 else "not-verified"
执行记录至少包含：输入表达式、假设、库版本、精确/近似模式、命令或脚本、输出、失败条件、claim level。
性能口径：符号表达式可能发生组合爆炸；矩阵稠密求解通常为 O(n^3)/O(n^2) 内存；批量数值优先 lambdify/向量化、稀疏结构和有界采样。
Examples
Example 1：恒等式检查
- 输入：
lhs = sin(x)^2 + cos(x)^2，rhs = 1。 - 动作：使用实变量假设和
trigsimp/simplify。 - 验收：记录 SymPy 版本与差值；状态最多
symbolically-checked。
Example 2：数值反例
- 输入：带参数的不等式猜想。
- 动作：先定义域，再用确定性网格与边界采样，保存首个反例。
- 验收：找到反例即
refuted-for-stated-domain；未找到只报告覆盖范围。
Example 3：大矩阵
- 输入：求解大型稀疏线性系统。
- 动作：识别稀疏性和条件数，优先 SciPy sparse solver，记录残差。
- 验收：没有构造不必要的稠密副本，报告时间/内存规模变量。
Example 4：GPU 预检与批量反例搜索
- 输入：对 10^8 个格点批量验证数值不等式猜想。
- 动作：先运行
python3 scripts/compute_plan.py --kind batch-search --n 1e8 --ops-per-sample 200 --dtype f32，按route选择 GPU 或 CPU；GPU 命中候选后用 SymPy/mpmath 精确复核。 - 验收：执行记录含路由决策、库版本、命中样本与复核结果；GPU 结果只标
numeric-check。
References
references/source-map.md：CAS、数值方法和 OEIS 来源映射。references/tool-catalog.md：数学工具、运行时、用法、profile 与证据边界。references/pressure-tests.md：数值/符号证据越权压力场景。
Maintenance
- Sources：
wentor-research-plugins数学技能、kdense-scientific-skills的 SymPy skill。 - Last updated：2026-08-16。
- Verification：
python3 scripts/smoke_math.py与python3 scripts/check_math_tools.py --profile <profile> --strict；库 API 以当前官方文档和实测为准。