math-olympiad

数学奥林匹克求解器

改变结果的五件事

1. 验证前先剥离思考过程 — 看到推理过程的验证者会偏向于认同。全新上下文，仅保留清洗后的证明。
2. “这是否证明了 RH？” — 如果你的定理在 ζ 上的特化是一个著名的开放问题，那么你就存在缺口。这是最可靠的警示信号。
3. 短证明 → 提取一般引理 — 尝试 2×2 反例。如果一般形式不成立，就找出 THIS 实例的特殊之处。
4. 同一个缺口出现两次 → 退后一步 — 情况拆分可能掩盖了一个统一的论证。三行有时能做到十二页做不到的事。
5. 说“没有确信的解答” — 错误且自信比诚实弃权更糟。

---

工具策略：在紧凑预算工作流中，求解器和验证器仅使用 THINKING。竞赛数学就是推理。计算用于深度模式（§6c），而且即便在那时也是有界的 — 一个双指数递归在 n~30 之后无法计算，改用 mod 2^m 计算。

---

何时使用哪种方法

问题	方法	验证
AIME 数值答案	Best-of-N → 多数投票	仅答案检查
奥林匹克证明（IMO/Putnam/USAMO）	下面的完整工作流	5 轮对抗式
“这个证明正确吗？”	跳到验证（第 4 步）	对抗式 + 规范博弈
完整题集（例如某场竞赛的全部 6 题）	顺序执行：每题一个完整工作流，收集结果，编译为单个 PDF	每题对抗式

在一个 Workflow 中批处理：为每个 agent() 调用设置 opts.label，使其包含题目 ID（例如 label: "P3:solver:2"）。没有标签时，返回的 36 个结果将无法与题目关联。并行运行题目 — 重要的是标签，而不是顺序。

对于完整题集

为每道题启动一个求解器工作流（相同的逐字提示词，不同的题目陈述）。并行运行它们。当全部返回后，对每道题运行对抗式验证。通过验证的题目其证明会进入 PDF；弃权的题目会得到“没有确信的解答”以及部分笔记。

不要试图在一个 Agent 的上下文中解决全部 N 道题 — 每道题都需要自己的思考预算和自己的全新上下文验证器。组合过程是机械的：收集每道题的输出，填入 LaTeX 章节，编译一次。 | “简化这个证明” | 跳到呈现（第 8 步） | — |

---

工作流

1. 解释检查（30 秒，可捕获某一类错误中的 50/63）

在求解任何东西之前，先确定解释。

阅读题目陈述。列出 2-3 种可能的解释方式。对每一种：这种解读是否 TRIVIAL？如果一种解读让题目变得简单，而另一种让它变得困难，那么困难的解读几乎肯定才是出题意图。说明你正在求解哪种解释，以及 WHY 你相信它是出题意图。

Aletheia 案例研究发现，63 个“技术上正确”的解答中有 50 个是针对错误解释的。奥林匹克题目常常有一个陷阱式的简单解读。

2. 通过内部精炼生成候选方案（并行，仅思考）

并行启动 8-12 个尝试 Agent。每个 Agent 在内部迭代—— 求解 → 自我改进 → 自我验证 → 修正 → 重复。这就是在 IMO 上达到 85.7% 的 Yang-Huang 结构：一次求解是不够的；每次尝试的精炼至关重要。

Agent 工具无法强制实施工具限制。 子 Agent 会获得完整的工具 集。唯一的机制是提示词。请逐字使用此提示词——不要 总结，不要自行合成：

NO COMPUTATION. Do not use Bash, Python, WebSearch, Read, Write, or any tool that runs code or fetches data. Numerical verification is not a proof step. "I computed n=1..10 and the pattern holds" is not a proof.

(If your agent harness requires a StructuredOutput or similar return-mechanism tool call, that is NOT a computation tool — call it to return your answer. The restriction is on tools that DO work, not tools that REPORT work.)

Your internal process (iterate until done):
- Solve: Complete rigorous solution.
- Self-improve: Reread. Fix gaps before a grader sees it.
- Self-verify: Strict grader mode. Every step justified?
- Correct: Fix and re-verify. Up to 5 rounds.
- Stop: Self-verify passes twice clean, OR 5 rounds, OR approach fundamentally wrong.

A correct answer from flawed reasoning is a failure. If incomplete, say so honestly. Never hide gaps.

PROBLEM: <insert the problem statement here>
ANGLE: <insert one starting angle here>

前两段是承重段落。一个会话若自己编写提示词 并省略它们，就会产生子 Agent 用 30 次迭代硬磨 Python 并 自信地得出错误答案——这种模式适用于 n≤10，但在 n=100 时会失败，这 不是证明。

起始角度（在各 Agent 之间变化——参见 references/solver_heuristics.md）：

• 推导小规模情形（测试超过 n=3 的情况）
• 寻找不变量或单调量
• 考虑极端情形
• 尝试归纳法
• 有哪些对称性？
• 反向推导
• 去掉一个条件——它在何处变得显然为假？
• 推广（发明者悖论——更多结构有时更容易）

每个 Agent 返回其最终状态（而非中间轮次）：

**Verdict**: complete solution | partial result | no progress
**Rounds**: [how many verify→correct cycles]
**Method**: [key idea, one paragraph]
**Detailed Solution**: [full step-by-step, every step justified]
**Answer**: [if applicable]
**Self-verification notes**: [what you caught and fixed; remaining concerns]

重试策略：如果某个 Agent 失败或超时，重试一次。瞬时失败 是会发生的。

3. 清理解答（上下文隔离——头号杠杆）

思考轨迹会使验证者偏向于认同——一长串 推理读起来像是支持性证据，即使结论是错误的。在任何验证之前，剥离：

• 所有 thinking 块内容
• 所有「让我试试……」／「实际上等等……」／「嗯」之类的文字
• 所有错误的开头和回溯

剩下的是：问题陈述 + 干净的最终论证。

仅从每个求解器的输出中提取 Method + Proof + Answer 部分。 验证者永远不会看到求解器是如何得到答案的。

4. 对抗性验证（全新上下文，模式武装）

对于每个清理后的解答，启动一个全新的验证者 Agent。全新上下文：它 只看到（问题陈述 + 清理后的解答）。不使用工具。

验证者的任务是攻击，而不是评分。加载 references/adversarial_prompts.md 获取提示词。它运行的关键模式：

模式	检查
#4	这个定理是否可特化到某个著名对象（ζ、二次互反律等）并证明关于它的某个未解决问题？→ 存在缺口
#18	将证明自身的中间恒等式代入任何「剩余缺口」。能否恢复原始命题？→ 同义反复
#40	是否有任何步骤是「一行引理」？提取其一般形式。寻找 2×2 反例。如果一般形式为假，找出是什么特殊结构拯救了此实例
#5	对于每个被调用的定理：从头重新检查其假设。「在 [0,1] 上连续」≠「在 ℝ 上连续」
#6	是否有任何无穷和通过正则化值被「界定」？检查边界——如果那里有极点，则该和发散

完整模式列表：references/verifier_patterns.md

验证者返回：

**Verdict**: HOLDS | HOLE FOUND | UNCLEAR

**If HOLE FOUND**:
- Location: [quote the problematic step]
- Pattern: [which check fired, or "other"]
- Why it breaks: [specific]
- Fixable?: [yes with X / no, fundamental]

5. 排序与投票验证（非对称 + 提前退出）

按（裁决、验证者置信度）对解决方案排序。取排名最高的一个。运行最多 5 个 全新的验证者 Agent。

非对称阈值：4 个 HOLDS 才能确认，2 个 HOLE FOUND 即可反驳。为什么 非对称：一个不稳定的验证者不应杀死一个正确的证明；但两个 独立的异议才是真正的信号。

鸽巢提前退出：一旦结果已定，就停止启动验证者。

• 2 个说 HOLE FOUND → 被反驳，停止（省下剩余 3 次调用）
• 4 个说 HOLDS → 已确认，停止（省下第 5 次）
• 在 3 个验证者之后：如果 2 个 HOLDS + 1 个 HOLE，再启动 2 个（结果未定）。如果 3 个 HOLDS + 0 个 HOLE，再启动 1 个（仍可能达到 4-1）。

双重上下文隔离：每个验证者对 (a) 求解者的思考 轨迹——已在步骤 3 中剥离——以及 (b) 其他验证者的裁决都不可见。每个 验证者都以为自己是第一个。没有“已有 3 个 Agent 确认过这个”的社交 证明。

求解者不能验证自己的解决方案。 不同的 Agent，全新的上下文。

5b. 当一个分支无法收尾时——在硬啃之前先退一步

如果一个证明分裂成若干分支，其中一个分支很容易证明，而另一个却久攻不下： 在硬啃那个困难分支之前，先问是否存在一条能让这个分裂消失的路径。

能救你的套路：困难分支的假设本身往往蕴含了关于你尚未审视的某个 中间对象 的强结论。直接使用那个蕴含，而不是原来的推理链。

具体形态：为受约束的函数 f 证明 f(n) ≤ cn，并按整除 f(n) 的素数 p 做分支 分裂。一个分支通过在 (ℤ/p^e)* 中的指数论证收尾。另一个分支久攻不下——群 结构相同，但算术并不矛盾。修复方法：把假设“p | f(n)”代回 支配方程，蕴含 f(p) = p 本身。一旦得到这一点，一个 Fermat+Dirichlet 论证就能在三行内解决两个分支。分支分裂是 一段弯路——它是在对一个变量做分裂，而该变量在假设之下取 一个已知值。

在卡在分支 B 时检查：

• 分支 B 的假设对其他输入处的 f 蕴含了什么？
• 是否有另一对 (a,b) 可以代入支配方程？
• 你是否证明得太多？（一个更简洁的矛盾需要更少的机器。）

这也是一个呈现环节的胜利：无分裂的证明既更短又更 通用。

6. 修订（如需要）

如果验证发现漏洞：启动一个修订者 Agent。它得到（清理后的 解决方案 + 验证者的漏洞报告）。仍然无法访问原始的思考—— 修订者从漏洞出发工作，而不是重读你如何到达那里。

A verifier found this issue in the proof:
[hole report]

Fix the proof. If the hole is fundamental (the approach doesn't work), say so and return **Verdict: no confident solution** with what partial progress remains.

For any step you cannot fully close, mark it inline: [GAP: specific description of what remains]. Gaps in the proof text, not in a separate list — they're greppable and the next reviser knows exactly where to look.

最多 3 个修订周期。然后对修订后的证明重新运行投票。

如果模式 #40 触发（一行证明太干净），修订者会得到一份更强的 简报——来自 references/adversarial_prompts.md §7 的 Adversarial Brief 模板。它强制一个二选一：“这个通用引理显然是假的（这里有一个 2×2 反例）——所以要么找出 THIS 这个情形的特殊之处，要么找出证明在哪里 断裂。”不能返回“看起来没问题。”

6c. 深度模式（当紧缩预算弃权时）

标准工作流是紧缩预算：8 个求解器，约 15 分钟，纯推理。当它弃权时，问题可能需要更多时间，而不是更多能力。

深度模式是一个单一的专注 Agent，具备：

• 无限时间 —— 没有挂钟时间压力
• 允许针对性计算 —— 模运算校验、小规模情形枚举、恒等式的符号验证。而不是探索性暴力搜索或无界递归。
• 以弃权原因作为起点 —— 如果验证器发现了具体的缺口，就从那里开始。如果求解器从未声称完成，就从它们部分证明的内容开始。

典型情形：一个专注的 Agent 拿到目前已证明的状态，外加“引理 5 有一个情形尚未解决”——然后找到一个 3 行的论证，而此前的情形划分恰恰掩盖了它。通常不到 10 分钟，且几乎不做计算。深度模式的关键在于给问题持续的注意力，而不是往上面堆算力。

深度模式不是什么：开放式探索、文献检索、查找解答、多日调查。那是另一种工作流（math-research）。深度模式仍然是“自己解决这个问题”——只是没有时钟。

禁止联网。禁止查找。 深度模式可以使用 Bash/Python 进行有界计算，但绝不使用 WebFetch、WebSearch 或任何网络访问。在 AoPS 或博客上找到解法不算解决问题——那是在奥数比赛中作弊，而且它无法让我们了解该技能的真实能力。把这一点放在深度模式提示词的最顶部：

NO WEB ACCESS. Do not use WebFetch, WebSearch, or any tool that touches the internet. Do not look up this problem, its solution, or related problems. You are solving this yourself — the only allowed computation is local (Bash/Python for mod-k arithmetic, small-case enumeration n≤10, symbolic identity checks). If you invoke a web tool, the proof is void.

深度模式中的计算边界（bug #8 的教训）：A6 的 b_{n+1}=2b_n²+b_n+1 是双指数的；b_99 约有 10^{2^98} 位数字。绝不要精确计算这类对象——在 ℤ/2^m 中工作，或只跟踪 v_p(·)，或对你关心的量证明该递推式在模意义下成立。如果某个计算运行超过 60 秒，它很可能是无界的。终止它，改用符号方法。

步骤 6d（非可选）：在验证阶段出现任何 ABSTAIN 之后，在将弃权写入输出之前，自动启动一个深度模式 Agent。给它：

• 问题陈述
• 来自紧缩预算求解器的最佳部分证明
• 验证器缺口描述（具体是什么没有闭合）
• 指令：“禁止网络访问——不要查找此问题或其解答。允许有界本地计算（mod 2^k、小规模情形 n≤10、仅通过 Bash/Python 进行符号恒等式校验）。60 秒计算限制。如果 n≤10 的暴力搜索揭示了紧缩预算求解器遗漏的模式，那个模式就是证明结构。”

深度 Agent 可能会找到纯推理求解器看不到的构造。如果它也弃权，那时才写入弃权。不要跳过这一步——答案为 √n 或 log n 的问题往往对纯推理不可见，因为最优结构是非对称的那一种。

编排器自我克制：编排器本身不得为了“帮助”深度 Agent 而对问题做网络搜索。如果你忍不住想 Fetch 一个 AoPS 帖子“只是为了核对答案”，别这么做——那会污染该技能的输出，并错误呈现其能力。

7. 校准弃权

如果 3 个修订周期全部失败：停下并承认。

**Verdict**: no confident solution

**What was tried**: [approaches]
**What WAS proven**: [any lemma or partial result that survived verification]
**Where it breaks**: [the unfixed hole]

不要猜。一个错误而自信的答案比一个诚实的“无法解决”更糟。真正重要的指标是条件准确率——当你说“已解决”时，你是对的吗？

8. 呈现环节（在正确性确立之后）

一份经核验正确的证明往往并不是一份漂亮的证明。你发现它的顺序很少是呈现它的最佳顺序。用一个全新的呈现 Agent 来处理这份已核验的证明。

加载 references/presentation_prompts.md。该 Agent 会问：

• 表达这一点的最简单方式是什么？
• 哪些引理应当内联？哪些值得单独列出？
• 有没有什么是过度设计？（在线性即可满足时却构造双重指数）
• 既然我们已经知道答案，是否存在一个 3 行的后见之明式证明？

输出：LaTeX 格式的证明。如果 pdflatex 可用（scripts/check_latex.sh 返回 0），还需通过 scripts/compile_pdf.sh 编译为 PDF。

---

模型档位默认值

完整细节请阅读 references/model_tier_defaults.md。摘要：

模型	求解器	验证轮次	弃权条件	呈现
Haiku	8	3	2 次修订失败	跳过
Sonnet	4	5	3 次修订失败	是
Opus	3	5 + 全模式扫描	4 次修订失败	2 份草稿，选更干净者

较弱的模型：更多并行尝试、更快弃权。较强的模型：更深入的验证、更多的呈现投入。

---

针对数值答案问题（AIME 风格）

跳过证明机制。用多种方法运行 5-7 个求解器，对数值答案取多数票。如果没有多数：通过代入验证排名前 2 的候选答案。

---

关键参考

• references/verifier_patterns.md — 12 项对抗性检查
• references/adversarial_prompts.md — 可直接使用的验证器提示词
• references/presentation_prompts.md — 美化提示词 + LaTeX 模板
• references/model_tier_defaults.md — 各模型配置

---

本方案与通用“验证并精炼”有何不同

1. 双重上下文隔离：验证器对 (a) 求解器的思考轨迹——这会带来偏向认同的偏差——以及 (b) 其他验证器的裁决——社会认同同样带来偏差——均不可见。每个验证器都以为自己是第一个。
2. 针对具体模式的攻击：不是问“这正确吗？”，而是问“这是否犯了 #40 错误？犯了 #4 错误？”具体胜过笼统。7 类反驳分类法为验证器提供了一份清单。
3. 非对称投票 + 鸽巢式退出：4 票确认，2 票反驳。一个不稳定的验证器不会杀死一份正确的证明；两票异议则会。一旦结果已定就停止启动验证器——在明确案例上节省约 30% 的验证成本。
4. 优先进行规范博弈检查：在求解之前明确询问“这是预期的解读吗？”。这是先前工作中排名第一的失败模式（50/63 个“正确”答案解错了题意）。
5. 校准式弃权：会带着部分结果说“没有可信的解答”。优化的是条件准确率，而非覆盖率。
6. 呈现环节：正确性和优雅性是分开的步骤。呈现 Agent 拿到的是已核验的证明，并找出表达它的最干净方式。