prove-protocol

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

prove-protocol — the full proving playbook

prove-protocol — 完整证明手册

0. The discipline, and why it is shaped like this

0. 这套纪律，以及它为何如此设计

Within this protocol, no mathematical claim is graded closed on agreement. It is graded VERIFIED-CLOSED only when an agent assigned to refute it — armed with executed exact arithmetic — has failed, and when a second agent who authored nothing has rebuilt the chain from the spec alone, reproducing every pre-registered value with fresh code. This is a working standard for agent output, not a substitute for a refereed or formally verified proof. Everything below is machinery for manufacturing those two events on purpose.

The paranoia is calibrated to three observations from practice and from the literature (Sources, below):

Agreement is free. Provers built on the same or similarly trained models share blind spots and converge on the same form — including the same wrong form. Consensus measures correlation of priors, not truth. Independence must be forced structurally (separate contexts, forbidden cross-reading, named-distinct routes), never requested in a prompt.
Self-review approves its own bugs. The reasoning that produced a flawed step is the same reasoning that re-reads it and finds it convincing.
Talk is a null instrument. Natural-language-only critique ("step 7 seems under-justified") does not move a proof's state — a measured null (the intrinsic self-correction null measured by Huang, Chen, Mishra, Zheng, Yu, Song and Zhou, arXiv:2310.01798, ICLR 2024). The only signal that cannot be socially generated is an executed exact computation at a hostile instance; every check in this protocol bottoms out in a script that ran.

Two regimes. Know which one you are in before spending tokens:

REGIME 1 — the statement is known: run the pipeline in §1 (target-pin → adversary-first hunt → prover/skeptic core → forced-diversity provers → fresh-context cross-verify → interface trace).
REGIME 2 — the statement is UNKNOWN or keeps dying: theory-finding (§4). The failure smell: you pin formulation after formulation and a competent adversary kills each within hours. A consistent pattern: target reshapings come from adversaries, essentially never from provers — provers do not find theorems; searchers and adversaries do.

在本协议中，任何数学命题都不会仅因达成一致而被判定为已闭合。只有当负责反驳它的 Agent——配备已执行的精确算术——未能反驳该命题，并且第二个未参与任何撰写的 Agent 仅依据规格重建整条推理链、使用全新代码复现每个预注册值时，该命题才会被判定为 VERIFIED-CLOSED。这是针对 Agent 输出的工作标准，不能替代经同行评审或形式化验证的证明。下文所有机制都是为了有意识地促成上述两种事件。

这种审慎程度是根据实践和文献（见下文来源）中的三项观察校准的：

一致是免费的。 基于相同或相似模型训练的证明者会共享盲点，并收敛到同一种形式——包括同一种错误形式。共识衡量的是先验之间的相关性，而不是真实性。必须从结构上强制实现独立性（分离上下文、禁止交叉阅读、明确指定不同路径），而不能只在提示词中请求独立。
自我审查会认可自己的错误。 产生错误步骤的推理，与重新阅读该步骤并认定它令人信服的推理是同一套推理。
交谈是一种零效应的工具。 仅靠自然语言的批判（例如“第 7 步似乎论证不足”）无法改变证明的状态——这是一种经测量为零的效应（Huang、Chen、Mishra、Zheng、Yu、Song 和 Zhou，arXiv:2310.01798，ICLR 2024，测得的内在自我纠错零效应）。唯一无法由社会性互动产生的信号，是在对抗性实例上执行的精确计算；本协议中的每项检查最终都落实到一个真正运行过的脚本上。

分为两种模式。在投入 token 之前，先确定自己处于哪一种模式：

模式 1——命题已知：运行 §1 中的流程（目标锁定 → 优先对抗搜索 → 证明者/怀疑者核心 → 强制多样性证明者 → 全新上下文交叉验证 → 接口追踪）。
模式 2——命题未知，或命题不断被推翻：进行理论发现（§4）。失败信号是：你锁定一个又一个表述，而一个称职的对抗者总能在数小时内将其推翻。其一致模式是，目标的重构通常来自对抗者，几乎不会来自证明者——证明者不会发现定理；搜索者和对抗者才会。

1. The pipeline core (REGIME 1)

1. 流程核心（模式 1）

ADVERSARY FIRST (X0) — reliably the highest-value step per token spent. Before any proving run, spend one run hunting the exact witness that makes the claim FALSE (in-regime, exact-arithmetic witness). Ladder discipline: shift the target ONLY on a certified fire (exact witness, inside the claimed regime); a NO-FIRE changes nothing. A certified kill is constructive — with pre-registered alternative forms (see step 1), the kill licenses the surviving form instead of ending the run.

Micro-example of the X0 posture. Claim: "over the whole family, the quantity is minimized at the symmetric configuration." The adversary does not read the heuristic argument; it writes a short exact enumerator over the family's smallest members and aims it where symmetry arguments die — degenerate members, boundary parameters, the smallest asymmetric instance. A minimizer that moves at a degenerate member is a certified kill, and the witness names the repair (exclude the degenerate class, or weaken to non-strict). One agent-run; it often saves ten.
TARGET-PIN as a shared SPEC: one spec file every prover reads, containing (a) the statement/hole verbatim with source citations; (b) a MAY-ASSUME list (granted lemmas WITH their stated hypotheses) and a MUST-NOT-ASSUME list (the thing being proven); (c) licensed alternative delivery forms WITH acceptance criteria ("closes the consuming target at the printed exponents; constants may be flagged, exponents may not move"); (d) an exact test instance T1 — pre-registered rational/integer values plus named FAIL conditions ("a route whose T1 prediction fails is DEAD"); (e) an erratum channel — specs contain bugs (independent arms have repeatedly falsified claims that turned out to be bugs in the spec itself, not the mathematics), so the spec must be correctable without invalidating prover runs already in flight. Pre-register which outcome changes what. The pin agent and the X0 adversary agent are SEPARATE agents — merging them invites an output-cap death; any stage mixing statement-extraction with construction dies.
SKEPTIC LOOP (the highest-yield loop in practice):
- ONE workfile is the sole shared state; pre-load the skeptic's danger list before proving starts.
- The PROVER drafts the full chain with every displayed identity tied to an executed exact-arithmetic script.
- A hostile fresh-context SKEPTIC does grounded spot-checks at adversarial instances and emits machine-readable bug reports —
```
{failing step index, exact instance, value of each side, residual}
```
  — never an essay. Prose-only critique counts for NOTHING.
- Revise against the report. Accept only after 2–3 CONSECUTIVE clean fresh-context passes.
- One SNEAKY-PLANT audit, on a COPY: plant a known-false step and verify the harness CATCHES it. If the plant survives, the harness is unfalsifiable and the arm is invalid.
- Any import outside MAY-ASSUME: flag it verbatim, verify it in the source, and PRE-REGISTER the downgrade path ("if ruled inadmissible → OPEN-AT step k with the rest intact"). This adversarial self-audit is what makes one-pass external verification possible.
FORCED-DIVERSITY RIDER (mandatory): ≥2 extra provers on named distinct routes, parallel fresh contexts, no cross-reading. Lesson from practice: independent arms converge unanimously on the same form with ease — and the artifact that reshapes a target tends to come only from a forced-divergent route, at any budget. The redundancy (including DNFs and failed certifiers) buys the one artifact nothing else produces. RULE: a closure without a diversity pass is graded PROVISIONAL. Cheap version: ONE skeptic chain (the proof) + ONE small tournament of 2–3 forced-distinct provers (the falsifier).
FRESH-CONTEXT CROSS-VERIFY + INTERFACE TRACE (both mandatory before VERIFIED-CLOSED). Every arm self-grades CLOSED-UNVERIFIED; nothing counts until BOTH: (a) verify pass: an agent that authored NOTHING re-derives the chain in its own words under hostile instructions, treats every "clearly" as a check-site, writes a FRESH independent enumerator (no code reuse) that reproduces every pre-registered exact value, and greps the load-bearing imports for circularity. Verdict: CONFIRMED / refuted, constants printed. (b) interface ruling: trace EVERY use-site of the delivered object in the consuming document; rule per-site whether the delivered form satisfies the consumer's STATED hypothesis (not its wording — wording is often shaped like the strong form over content the weak form covers); machine-check the composed arithmetic. This is where an alternative-form delivery gets legitimized or killed.

ADVERSARY FIRST (X0)——通常是每单位 token 投入中价值最高的一步。在任何证明运行之前，先用一次运行搜寻能够令命题为 FALSE 的精确见证（在命题声称的适用范围内，以精确算术给出见证）。阶梯纪律：只有在出现经认证的触发时（在适用范围内找到精确见证）才能改变目标；NO-FIRE 不改变任何内容。经认证的否决具有建设性——结合预注册的替代形式，一次否决会授权采用仍然存活的形式，而不是直接终止运行。

X0 姿态的微型示例。 命题：“在整个参数族中，该量在对称配置处取得最小值。”对抗者不阅读启发式论证；它针对参数族中最小的若干成员编写一个简短的精确枚举器，并瞄准对称性论证失效的位置——退化成员、边界参数、最小的非对称实例。如果极小点会在退化成员处发生移动，这就构成一次经认证的否决；该见证同时指出修复方式（排除退化类别，或弱化为非严格形式）。只需一次 Agent 运行；它往往能节省十次运行。
将 TARGET-PIN 作为共享 SPEC：建立一个所有证明者都会读取的规格文件，其中包含：(a) 逐字记录命题/待补缺口及其来源引用；(b) MAY-ASSUME 清单（授予的引理及其明示假设）和 MUST-NOT-ASSUME 清单（当前正在证明的内容）；(c) 获准采用的替代交付形式及其验收标准（“以打印出的指数闭合消费端目标；常数可以标记，但指数不得移动”）；(d) 一个精确测试实例 T1——预注册的有理数/整数值，以及明确命名的 FAIL 条件（“任何 T1 预测失败的路径均为 DEAD”）；(e) 一个勘误通道——规格本身也可能包含错误（独立分支曾多次证伪某些命题，最终发现错误来自规格本身而非数学），因此必须能够在不使已在进行中的证明运行失效的情况下修正规格。预先注册每种结果分别会改变什么。锁定 Agent 与 X0 对抗者必须是不同的 Agent——合并二者会招致 output-cap 式的失败；任何把命题提取与证明构造混在一起的阶段都会失败。
SKEPTIC LOOP（实践中收益最高的循环）：
- 一个工作文件是唯一的共享状态；证明开始前先载入怀疑者的风险清单。
- 证明者起草完整推理链，其中每个展示出来的等式都对应一个已执行的精确算术脚本。
- 一个采用全新上下文的敌对怀疑者会在对抗性实例上进行有依据的抽查，并输出机器可读的缺陷报告——
```
{有缺陷的步骤索引, 精确实例, 两侧的值, 残差}
```
  ——绝不写长篇评论。仅有文字的批判毫无价值。
- 根据报告修改推理。只有在全新上下文下连续 2–3 次无问题通过后，才能接受结果。
- 在一份副本上执行一次 SNEAKY-PLANT 审计：植入一个已知错误的步骤，并验证验证框架能够捕捉到它。如果植入的缺陷仍然存活，说明该验证框架不可证伪，该分支无效。
- 任何来自 MAY-ASSUME 之外的导入：逐字标记、在来源中核验，并预注册降级路径（“如果被裁定为不可采纳 → 在第 k 步保持 OPEN，其余部分保持有效”）。这种对抗式自审使一次通过式外部验证成为可能。
FORCED-DIVERSITY RIDER（强制执行）：至少增加 2 名证明者，要求其采用明确指定的不同路径，在并行的全新上下文中工作，且不得交叉阅读。实践教训是：独立分支很容易一致收敛到同一种形式——而能够重构目标的产物通常只来自一条被强制分化的路径，无论预算多少。这种冗余（包括 DNF 和失败的验证器）能够获得其他任何方式都无法产生的唯一产物。规则：没有经过多样性环节的闭合只能评为 PROVISIONAL。低成本版本：一条怀疑者推理链（即证明）＋一场由 2–3 名强制差异化证明者组成的小型竞赛（作为证伪者）。
全新上下文交叉验证 + 接口追踪（在判定 VERIFIED-CLOSED 前，两者均为必做项）。每个分支都先自行评为 CLOSED-UNVERIFIED；只有同时完成以下两项，结果才有效：
- (a) 验证环节：一个未参与任何撰写的 Agent 在敌对指令下用自己的语言重新推导整条推理链，把每一个“显然”都视为检查点，编写一个全新的独立枚举器（不得复用代码）以复现每个预注册的精确值，并检查所有承重导入是否存在循环依赖。裁决：CONFIRMED / refuted，并打印相关常数。
- (b) 接口裁定：追踪交付对象在消费文档中的每一个使用位置；逐一裁定交付形式是否满足消费者明示的假设，而不是其文字表述——文字往往被写成强形式，而弱形式实际已经覆盖了其内容。对组合后的算术进行机器检查。替代形式的交付正是在这里获得认可或被否决。

2. Failure-mode catalogue

2. 失效模式目录

Each class is the reason a rule above exists; the vignettes describe mechanisms, not one-off accidents.

Proof by agreement. Provers converge on the same conclusion and the convergence is filed as verification. Mechanism: shared priors produce identical errors at any N — the agreement was determined before the first token was generated. Cure: §1.3 forced diversity plus §1.4(a); a verdict only counts from an agent that could have profited by disagreeing.
Steps verified by their author. The prover "double-checks" its own chain and reports all steps sound. Mechanism: the blind spot that wrote the bug re-approves it. Cure: skeptic and verifier are fresh contexts that authored nothing, always.
The skipped hunt. No counterexample search was run because the claim "obviously" holds — the heuristic is clean and the small cases in the prover's head work. Mechanism: obviousness is a fact about the prover's prior, not about the statement; the witness usually lives exactly where the intuition was trained not to look (degenerate and boundary instances). Cure: X0 is unconditional; it runs first even when everyone is sure.
Talk-only skepticism. The skeptic writes paragraphs of doubt, the prover writes paragraphs of reassurance, the workfile grows, the proof state does not move. Mechanism: language models happily co-author confidence. Cure: bug reports are machine-readable; anything without an executed instance is noise.
The harness that cannot fail. The verification loop passes everything — because it would pass anything. Mechanism: a checker that has never caught a planted bug has an unmeasured false-negative rate; its passes carry no information. Cure: the sneaky-plant audit — no trust before a demonstrated catch.
The silent import. Somewhere in step 9 the chain uses a fact outside MAY-ASSUME — often a disguised paraphrase of the target itself. Mechanism: circularity arrives dressed as a "standard fact." Cure: the verbatim import flag (§1.2) plus the verify pass's circularity grep.
The unexecuted certificate. The journal says "the attached script verifies this" and the script was never run to completion; one measured "certificate" failed its own pre-registered asserts when actually executed. Mechanism: writing a plausible checker and running one are different acts. Cure: script-of-record with output quoted verbatim (§3).
Verification against wording. An alternative-form delivery is accepted (or rejected) because it matches the consumer's sentence rather than its hypothesis. Mechanism: statements are routinely written stronger than their proofs use. Cure: the interface trace (§1.4b).
The spec trusted as ground truth. All arms faithfully attack a statement mis-transcribed at pin time — an index off by one, a hypothesis dropped. Mechanism: the pin has the same error rate as any other artifact. Cure: the erratum channel; treat a unanimous early kill as a possible spec bug first.
Pin-thrash (the zombie statement). The tenth reformulation of a repeatedly-killed claim is being pinned with fresh hope. Mechanism: the true object is usually a continuum or a mechanism, not the crisp dichotomy being re-pinned; each new pin samples the same doomed neighborhood. Cure: switch to REGIME 2 (§4).

每一类失效都是上述某条规则存在的原因；这些案例描述的是机制，而不是孤立事故。

靠一致完成的证明。 证明者收敛到同一结论，并把这种收敛归档为验证。机制：共享先验在任何 N 下都会产生完全相同的错误——这种一致在第一个 token 生成之前就已经确定。解决方案：§1.3 的强制多样性以及 §1.4(a)；只有可能因提出异议而获益的 Agent，其裁决才具有效力。
由作者自行验证的步骤。 证明者“再次检查”自己的推理链，并报告所有步骤都正确。机制：写下错误的盲点会再次认可该错误。解决方案：怀疑者和验证者始终采用未参与任何撰写的全新上下文。
被跳过的搜索。 因为命题“显然”成立，所以没有运行反例搜索——启发式论证看起来干净，而且证明者脑中的小规模案例也都成立。机制：显然性是证明者先验的事实，而不是命题的事实；见证通常恰好存在于直觉被训练为不会去看的那些位置，即退化和边界实例。解决方案：X0 是无条件必做项；即使所有人都很有把握，它也必须首先运行。
只靠交谈表示怀疑。 怀疑者写下几段怀疑，证明者写下几段保证，工作文件不断增长，证明状态却没有变化。机制：语言模型乐于共同制造信心。解决方案：缺陷报告必须采用机器可读格式；任何没有已执行实例的内容都只是噪声。
永远不会失败的验证框架。 验证循环会放过所有内容——因为它会放过任何内容。机制：一个从未捕捉到植入缺陷的检查器具有未测量的假阴性率；它的通过不包含任何信息。解决方案：执行 sneaky-plant 审计——在证明能够捕捉缺陷之前，不予信任。
隐蔽的导入。 推理链在第 9 步之类的位置使用了 MAY-ASSUME 之外的事实——通常是对目标本身的 disguised paraphrase（换个说法的改写）。机制：循环依赖会伪装成“标准事实”出现。解决方案：逐字标记导入（§1.2），并在验证环节中检查循环依赖。
未执行的证书。 日志声称“附带脚本已验证此结果”，但脚本从未完整运行；一个经过测量的“证书”在实际执行时，未能通过自身预注册的断言。机制：编写一个看似合理的检查器与真正运行它是两种不同的行为。解决方案：使用记录脚本，并在日志中逐字引用其输出（§3）。
按文字而非按含义验证。 替代形式的交付之所以被接受或拒绝，是因为它与消费者的句子相符或不符，而不是因为它符合或不符合消费者的假设。机制：陈述的措辞经常强于其证明实际使用的内容。解决方案：接口追踪（§1.4b）。
把规格当作绝对真理。 所有分支都在忠实攻击一个锁定时被错误转录的命题——例如索引偏移一位，或遗漏了一个假设。机制：锁定过程与其他任何产物具有相同的错误率。解决方案：设置勘误通道；将早期的一致否决首先视为潜在的规格错误。
锁定反复横跳（僵尸命题）。 一个不断被推翻的命题已经被重新表述了十次，却仍被带着新的希望重新锁定。机制：真正的对象通常是一个连续体或一种机制，而不是被反复锁定的清晰二分法；每次新的锁定都只是在同一个注定失败的邻域中采样。解决方案：切换到模式 2（§4）。

3. Infrastructure rules (each learned from an agent failure)

3. 基础设施规则（每一条都来自 Agent 失败教训）

Skeleton-first, corrected form (a recurring agent failure shape: bulk-read everything, then die at the output cap having planned but never written): (1) read the TARGET PIN ONLY; (2) IMMEDIATELY write the workfile skeleton, one pre-filled line per planned section; (3) read supporting files ONE AT A TIME, per section, transcribing each check into its section before opening the next file. Never hold more than one unwritten conclusion. For symbolic work: scripts write their own output files; quote ≤5-line summaries; never paste large expressions into messages.
Never steer a running proof agent mid-run — corrections go in relaunch prompts. Mid-run messages trigger a fatal re-planning burst.
Disk-incremental journals with executed evidence: the workfile is the proof state; write as you go. Transient infrastructure errors are not state changes — resume, never re-derive. A run that dies with zero bytes on disk is ungradeable: no journal = no arm. Script-of-record + output file quoted VERBATIM in the journal, so graders can replay exactly.
AMBIGUOUS-refusal beats silent improvisation: on a broken or ambiguous spec, halt-and-flag or redesign-with-logged-deviation (legal, gradeable). Silently improvising out-of-model parameters is a measured downgrade-to- OPEN.
Detach all compute expected to outlive the agent's turn (e.g. setsid/nohup or your framework's background-job facility); non-detached children die with the tool session.
Budget honesty: parallelism premium charged; DNFs and failed certifiers count against the arm; the metric is reusable-progress-per-token, not closure count.

先搭骨架，再采用修正后的形式（一种反复出现的 Agent 失败形态：批量读取所有内容，随后在输出上限处死亡，虽然已经制定计划，却从未真正写出内容）：(1) 只读取 TARGET PIN；(2) 立即写出工作文件骨架，每个计划中的章节预先填写一行；(3) 按章节逐个读取支持文件，每打开下一个文件之前，先把该项检查誊写到对应章节。绝不让超过一个尚未写出的结论停留在上下文中。对于符号工作：脚本应自行写出输出文件；引用不超过 5 行的摘要；绝不把大型表达式粘贴到消息中。
绝不在证明 Agent 运行期间对其进行引导——修正应写入重新启动的提示词。运行中的消息会触发致命的重新规划爆发。
使用带有执行证据的磁盘增量日志：工作文件就是证明状态；边执行边写入。瞬时基础设施错误不构成状态变化——应恢复运行，而不是重新推导。若一次运行在磁盘上留下零字节，则无法评分：没有日志就没有分支。记录脚本及其输出文件必须在日志中逐字引用，以便评分者能够精确重放。
宁可明确拒绝有歧义的任务，也不要默默即兴发挥：面对损坏或含糊的规格，应停止并发出标记，或重新设计并记录偏离（这种做法合法且可评分）。默默引入模型未设定的参数，会被明确降级为 OPEN。
分离所有预计会超出 Agent 当前轮次生命周期的计算任务（例如使用 setsid/nohup，或框架提供的后台作业机制）；未分离的子进程会随工具会话一起终止。
预算必须诚实：并行执行需要支付额外成本；DNF 和失败的验证器都要计入该分支的成本；衡量指标是可复用进展/token，而不是闭合数量。

4. THEORY-FINDING (REGIME 2 — when the statement itself is unknown)

4. 理论发现（模式 2——命题本身未知时）

The signature of this regime: formulation after formulation gets hand-pinned, and a competent adversary kills each one within hours or days. When repeated pins die, STOP hand-guessing and search statement-space mechanically:

4a. Build the exact evaluator first (the FunSearch / AlphaEvolve precondition: generate-and-score against an exact evaluator is the pattern behind the published machine-discovered mathematics we know of — Romera-Paredes et al., Nature 625 (2024) 468, doi:10.1038/s41586-023-06924-6; Novikov et al., arXiv:2506.13131; Georgiev, Gómez-Serrano, Tao and Wagner, arXiv:2511.02864). Assemble a LABELED CORPUS of every certified object the effort has produced (witnesses, counterexamples, controls; label quality = certified/measured/screened as an explicit field, receipt-traced). Then a FEATURE LIBRARY of computable functionals spanning the project's mechanistic vocabulary. The corpus + evaluator turn "is this candidate statement true so far?" into an exact, instant check.

4b. Forced-distinct THEORY TOURNAMENT: 2–4 agents, no cross-reading, each LOCKED to a different organizing principle (e.g., bifurcation / symmetry-breaking; information geometry; real algebraic geometry; probabilistic / genericity). Each must deliver: the organizing picture in its lens; CANDIDATE THEOREMS fully quantified and falsifiable; an explicit object-by-object consistency table against the certified corpus; the 3 sharpest first tests; honest scoping of which certified objects fall outside its lens. Divergence between arms is data.

4c. Invariant synthesis over the feature matrix (searchers: sparse inequality synthesis, monotone-lattice search, program search) — candidates scored by the exact evaluator, survivors handed IMMEDIATELY to an X0 adversary — never pin a synthesized statement that has not survived a dedicated falsification run.

4d. Formulation-ladder bookkeeping: every dead formulation gets its killer recorded (witness + mechanism). The kill LIST is itself a deliverable — after enough kills it becomes a theorem-grade impossibility map, and the mechanisms usually name the surviving statement's true shape (in practice the kills typically trace to a small number of identifiable degeneracy structures).

这一模式的特征是：手工锁定一个又一个表述，而一个称职的对抗者总能在数小时或数天内将每个表述推翻。当多次锁定都失败时，停止手工猜测，改为机械搜索命题空间：

4a. 首先构建精确评估器（这是 FunSearch / AlphaEvolve 的前提：针对精确评估器进行生成并评分，是目前已发表的机器发现数学成果背后的模式——Romera-Paredes 等，Nature 625 (2024) 468，doi:10.1038/s41586-023-06924-6；Novikov 等，arXiv:2506.13131；Georgiev、Gómez-Serrano、Tao 和 Wagner，arXiv:2511.02864）。建立一个带标签的语料库，涵盖该工作迄今产出的所有经认证对象（见证、反例、对照对象；将标签质量设为 certified/measured/screened 的显式字段，并确保可通过凭证追溯）。随后建立一个特征库，其中包含覆盖项目机制性词汇的可计算泛函。语料库与评估器共同把“目前这个候选命题是否成立”转化为精确的即时检查。

4b. 强制差异化的理论竞赛：安排 2–4 个 Agent，禁止交叉阅读，每个 Agent 都锁定一种不同的组织原则（例如分岔/对称性破缺、信息几何、实代数几何、概率性/泛性）。每个 Agent 都必须交付：其视角下的组织图景；经过完整量化且可证伪的候选定理；针对经认证语料库、逐个对象编写的显式一致性表；最锐利的 3 项初步测试；以及哪些经认证对象不在其视角范围内的诚实界定。分支之间的差异本身就是数据。

4c. 在特征矩阵上进行不变量综合（搜索器包括稀疏不等式综合、单调格搜索和程序搜索）——使用精确评估器为候选结果评分；存活者立即交给 X0 对抗者——绝不能锁定一个尚未通过专门证伪运行的综合命题。

4d. 管理表述阶梯的账目：记录每个失败表述的“杀手”，包括见证和机制。否决清单本身就是一项交付物——积累足够多的否决后，它会变成一份定理级的不可能图谱；这些机制通常会指出存活命题的真实形态。实践中的否决通常会追溯到少数几种可识别的退化结构。

5. Preconditions & priors (do not deploy blind)

5. 前置条件与先验（不要盲目部署）

Published base rates without preconditions, as of the cited evaluations (Mar 2025 / Feb 2026; capabilities move quickly): 10-15% cold success (pass@1) on fresh self-contained research lemmas (LemmaBench — Peyronnet, Gloeckle and Hayat, arXiv:2602.24173); <5% average proof score on USAMO 2025 for most models evaluated at release despite strong final-answer benchmark results (Proof or Bluff — Petrov, Dekoninck, Baltadzhiev, Drencheva, Minchev, Balunović, Jovanović and Vechev, arXiv:2503.21934). Projects beat the base rate only when THREE preconditions held — check all three first:

Exact-computable test instance: T1 with exact rationals, fully enumerable in seconds — every chain and every bug falsifiable by a CAS the same hour. Absent this, the skeptic loop degenerates to natural-language self-critique (measured null).
A falsifiable, pre-registered alternative: both forms NAMED in the spec with acceptance criteria, so the adversary has a concrete statement to kill and a kill constructively licenses the survivor. Absent this, the adversary step has no target.
Mature interface: the consumers of the result already exist with stated hypotheses and a may-assume list — quantifier-completion against known consumers, not open-sea invention. Absent this, expect the ~15% prior. For REGIME 2 add: (4) a corpus of certified objects rich enough to score candidates — if you lack one, run adversary/instance-building rounds first.

根据所引用的评测（截至 2025 年 3 月/2026 年 2 月；能力演进速度很快），如果不满足前置条件，已发表的基准成功率如下：对于新的自包含研究引理，冷启动成功率（pass@1）为 10%–15%（LemmaBench——Peyronnet、Gloeckle 和 Hayat，arXiv:2602.24173）；对于发布时评测的大多数模型，尽管最终答案基准成绩较强，USAMO 2025 的平均证明分数仍低于 5%（Proof or Bluff——Petrov、Dekoninck、Baltadzhiev、Drencheva、Minchev、Balunović、Jovanović 和 Vechev，arXiv:2503.21934）。

只有同时满足以下三项前置条件，项目才可能超过基准成功率——请先检查全部三项：

可精确计算的测试实例：T1 使用精确有理数，并可在数秒内完全枚举——每条推理链和每个缺陷都能在当天通过 CAS 证伪。如果缺少这一项，怀疑者循环就会退化为自然语言式的自我批判（经测量为零的效应）。
可证伪且已预注册的替代形式：两种形式都在规格中明确命名，并附带验收标准，使对抗者拥有一个可以具体推翻的命题，而一次否决能够有建设性地授权采用存活形式。如果缺少这一项，对抗步骤就没有目标。
成熟的接口：结果的使用者已经存在，并具有明示假设和 may-assume 清单——应面向已知使用者补全量词，而不是在公海中发明概念。如果缺少这一项，应预期只能达到约 15% 的先验成功率。

对于模式 2，还要增加：(4) 一个足够丰富的经认证对象语料库，用于为候选项评分——如果缺少它，应先运行对抗/实例构建轮次。

6. What has worked in practice, and what has not

6. 实践中什么有效，什么无效

WORKS (in our campaigns and in the literature cited in §5): generate-against-exact-evaluator; self-contained stuck-step consultation with CAS re-derivation; candidate-object search for analysis proofs (Lyapunov/ansatz enumeration, falsify-each-cheaply); decomposition into sublemma STATEMENTS first, split-on-verification-failure; literature retrieval (typed as retrieval, never as discovery). HAS NOT WORKED, for us or at the base rates cited in §5: autonomous end-to-end proving without a mechanical certifier; self-reported confidence; final-answer benchmarks as proving ability; natural-language-only critique.

Grading: VERIFIED-CLOSED only after §1.4's two passes. Log every run — arm, budget, grade, artifacts — to a scoreboard so DNFs and failed certifiers stay visible.

Sources and acknowledgments. This protocol was distilled from our own multi-agent proving campaigns, but its parts have antecedents we are glad to name: the verification-and-refinement loop of Huang and Yang (arXiv:2507.15855) and the practitioner techniques collected by Woodruff, Cohen-Addad et al. (arXiv:2602.03837) — problem decomposition, iterative refinement against error feedback, and the model deployed as an adversarial reviewer of existing proofs; counterexample-guided inductive synthesis (Solar-Lezama, Tancau, Bodik, Seshia and Saraswat, ASPLOS 2006) for the adversary/prover alternation; mutation testing (DeMillo, Lipton and Sayward, IEEE Computer 11(4) (1978) 34) for the planted-bug audit; Knight and Leveson's (IEEE Trans. Softw. Eng. SE-12 (1986) 96) demonstration that independently written versions fail together, which is why diversity is forced rather than requested; and, older than all of these, Lakatos's Proofs and Refutations (Cambridge, 1976). The exact-evaluator regime follows FunSearch and AlphaEvolve (refs in §4a); the base rates are from LemmaBench and Proof or Bluff (§5) and the self-correction null from Huang et al. (§0).

有效做法（基于我们的实践以及 §5 引用的文献）：针对精确评估器进行生成；围绕卡住步骤开展自包含咨询，并使用 CAS 重新推导；针对分析证明搜索候选对象（Lyapunov/ansatz 枚举、以低成本逐一证伪）；优先将问题拆分为子引理 STATEMENT，再按验证失败之处继续拆分；文献检索（明确归类为检索，绝不视为发现）。

无效做法（对我们或 §5 引用的基准成功率而言）：没有机械验证器时进行自主端到端证明；自我报告置信度；把最终答案基准当作证明能力；仅依靠自然语言进行批判。

评分：只有在完成 §1.4 的两个环节后才能判定为 VERIFIED-CLOSED。记录每次运行——分支、预算、等级和产物——并写入记分板，以确保 DNF 和失败的验证器始终可见。

来源与致谢。 本协议提炼自我们自己的多 Agent 证明实践，但其各个组成部分都有值得明确提及的先例：Huang 和 Yang 的验证与改进循环（arXiv:2507.15855）；Woodruff、Cohen-Addad 等收集的实践技术（arXiv:2602.03837）——问题分解、基于错误反馈的迭代改进，以及将模型作为现有证明的对抗性审查者；反例引导的归纳综合（Solar-Lezama、Tancau、Bodik、Seshia 和 Saraswat，ASPLOS 2006），用于对抗者/证明者交替；变异测试（DeMillo、Lipton 和 Sayward，IEEE Computer 11(4) (1978) 34），用于植入缺陷审计；Knight 和 Leveson 关于独立编写的版本会共同失败的证明（IEEE Trans. Softw. Eng. SE-12 (1986) 96），这也是必须强制而非请求多样性的原因；以及比这些都更早的 Lakatos 的 Proofs and Refutations（Cambridge，1976）。精确评估器模式源自 FunSearch 和 AlphaEvolve（参考文献见 §4a）；基准成功率来自 LemmaBench 和 Proof or Bluff（§5），自我纠错零效应来自 Huang 等（§0）。