数学搜打撤：结果主导的 AI for Math 研究搜索法

摘要

数学搜打撤是一种面向 AI for Math 的结果主导研究搜索法。它不把开放问题压成一次长提示词，也不把某个模型、证明技巧或计算工具当作默认路线；它先冻结问题语义，再展开可能改变研究状态的候选结果，选择少量互补前沿，围绕明确义务执行有界攻防，最后依据独立证据决定闭合、换路或撤离。

这套方法依赖一组可检查接口：形式化方法、Lean 等证明助手、可复现代码执行、CAS、SAT/SMT、证书检查器和版本化研究对象。生成系统扩大候选空间，形式化与可执行系统压缩错误空间，证据门决定哪些候选能够进入 Result。

方法的三个动作是：

• 搜（Search）：建立 ProblemContract 和 Outcome Graph，选择有界 Pareto frontier；
• 打（Strike）：按 Project → Workflow → Task → Step → Job 推进生成、攻击、修补和验证；
• 撤（Withdraw）：保存 Result、FailedRoute 或 checkpoint，终止无效消耗，并把新信息带回下一轮搜索。

“撤”承担研究记忆和资源纪律。一次失败若能留下可复核的障碍、适用范围和重启条件，就已经缩小了后续搜索空间。

一、研究问题：AI 数学缺少什么

1. 从文本生成到可裁决研究

大模型能够提出证明草稿、反例方向、代码和文献线索，但“生成了一段看似合理的数学文本”与“得到一个可以承担结论的数学结果”之间仍有很长的验证链。

开放数学研究至少面对四类不确定性：

1. 语义不确定性：模型处理的是否是原题，定义、量词和假设是否发生漂移；
2. 搜索不确定性：哪些结果值得优先追求，哪些路线只是重复已知死路；
3. 执行不确定性：程序、solver 或证明助手实际运行了什么，覆盖范围和资源边界是什么；
4. 证据不确定性：候选由谁验证，验证能力是否适用，结论能否传播到根问题。

如果没有结构化约束，研究容易退化成活动清单：继续推导、扩大枚举、再开一个会话、换一个模型。活动持续增加，问题状态却没有可审计变化。

2. 结果主导的研究规划

结果主导先问：

哪个可验证结果一旦成立或失败，会最大幅度改变我们对问题和搜索空间的认识？

因此，规划顺序被反转为：

定义值得获得的 Outcome
  → 写清 statement、scope 和 closure predicate
  → 判断它对根问题和其他节点的作用
  → 选择 route、owner、tool 和 budget
  → 在证据边界内执行

完整证明、全局反例、等价归约、特殊情形、必要条件、定量界、显式构造、方法障碍和题面修订，都可以成为候选结果。“尝试归纳法”“跑更多样例”“让模型继续思考”属于活动描述；它们缺少独立闭合判据，因此留在过程记录中。

3. 方法的四个核心判断

数学搜打撤建立在四个判断上：

• 形式化和可执行验证构成技术基础，语言生成负责提供候选；
• 候选结果构成搜索单位，模型调用和工具调用归入执行活动；
• 有界义务构成执行单位，自治进程必须服从期限和预算；
• 数学状态只由适用证据改变，不由聊天、commit、PR、CI 或运行结束改变。

二、技术基础：形式化方法与可执行验证

1. 语义形式化：先固定问题身份

形式化并不从编写 Lean 定理才开始。第一步是把自然语言题面转成版本化的 ProblemContract，明确：

• statement、domain 和 quantifiers；
• definitions、assumptions 和 allowed axioms；
• 来源、版本和新颖性边界；
• acceptance predicate；
• statement digest 与 scope digest；
• 允许的验证能力和执行预算。

如果题面身份不稳定，同一份程序或证明可能在不同版本的命题之间漂移。即使代码成功退出或 Lean 编译通过，也无法回答它是否处理了原问题。

来源页面中的 open、solved、answered 或奖金状态只是 SourceObservation。它们不能替代项目内部的 Evidence 或 Result。

2. 结构形式化：把“思路”变成对象和关系

OutcomeNode、Obligation、CandidateArtifact、EvidenceLink、Result、FailedRoute、Task 和 Job 都必须拥有类型、身份、作用域和关系。

候选结果至少通过

(statement_digest, scope_digest)

区分“说了什么”和“在什么范围内说”。陈述相同但范围不同，应保留为不同节点；一个候选包含多个不能共享闭合谓词的目标时，应拆成多个原子 Outcome；标题相似或 embedding 接近，只能触发语义审查，不能自动建立等价。

结构形式化使模型输出从一段不可定位的文字，变成可以关闭、反驳、失效和重放的研究对象。

3. 证明形式化：Lean 的位置

Lean 是开源编程语言和证明助手。它允许研究者精确表达定义、命题、依赖和证明项，并由小型受信内核检查 proof term 是否证明了给定形式命题。

在搜打撤中，AI 可以提出 Lean statement、lemma、tactic 或 proof term；Lean 内核对证明项的接受或拒绝，以及公理和声明依赖，都会形成可观察反馈。相比自然语言自评，这种反馈具有明确的机械语义。

但是，对形式化成果的评估不能只看 kernel_check=passed。证明助手确认的是：

这个证明项在给定环境中证明了这个形式命题。

它不能独立确认：

这个形式命题忠实表达了原始自然语言数学问题。

因此，kernel_check 与 statement_faithfulness 必须分轴记录。类型检查通过不能替代定义、量词、类型和题面映射的语义复核。

4. 计算形式化：代码执行的位置

代码执行把有限枚举、反例搜索、符号变换、定量优化、构造和证书生成变成可重复实验。一次可用执行至少绑定：

• 输入对象及其摘要；
• 源码、依赖和工具版本；
• 运行环境与随机种子；
• 时间、内存和搜索范围；
• 标准化输出、退出状态和产物摘要；
• 独立重放或证书检查入口。

代码作为独立的认识工具参与研究。它可以发现规律、生成 witness、击破辅助引理、验证有限范围、优化构造，也可以产生由更小检查器消费的 certificate。

代码证据的上限由算法和覆盖范围决定：有限扫描不能单独证明无限全称命题；浮点近似不能自动承担精确等式；启发式搜索没有找到反例，不等于反例不存在。

5. 多层验证栈

形式化与执行能力可以组织为逐层收紧的验证栈：

自然语言候选
  → ProblemContract / Schema 检查
  → 有界代码执行与独立重放
  → CAS / SAT / SMT / certificate 检查
  → Lean 等证明助手的 kernel check
  → statement-faithfulness 与适用性审查
  → EvidenceLink / Result 准入

各类成果调用与其匹配的验证层。一个显式有限反例可能由独立检查器充分验证；一般性证明可能需要形式证明或等价强度的复核；来源修订主要依靠文献和语义审查。证据记录必须写清实际检查内容和未覆盖范围，统一的“verified”标签无法承担这些信息。

6. AI 在验证栈中的职责

AI 的优势位于搜索和表示转换：

• 扩展候选结果；
• 发现不同表述和归约；
• 生成程序、证明草稿和形式化候选；
• 对候选实施对抗性攻击；
• 根据失败反馈修补局部节点；
• 把非结构化批评改写为新 Obligation。

AI 不应同时充当候选生成者、唯一验证者和最终裁决者。生成与评价必须分离，评价与 Result 准入也必须分离。

三、概念架构：PLFB、OSPS 与 PWTSJ

1. PLFB 是唯一元模型根

VibeMath 用 Point–Line–Face–Body（点—线—面—体，PLFB）统一研究对象。OSPS、PWTSJ、ProblemContract、Evidence 和 Result 都归入 PLFB 的面或面内模型，PLFB 保持唯一元模型根。

• Point：有稳定身份和类型的对象；
• Line：两个点之间有方向、有类型的关系；
• Face：一类事实的责任边界；
• Body：跨面引用形成的整体视图。

Body 只保存引用、版本和摘要，不复制 owner truth source。这样既能组合全景，也避免同一题面、证据或结果出现多份冲突副本。

2. 四张图与一本账本

一项研究至少分开：

• Semantic Graph：题面、定义、量词、假设和来源；
• Outcome Graph：候选结果、关系、阻塞和搜索前沿；
• Process Graph：Project、Workflow、Task、Step 和 Job；
• Evidence Graph：候选、验证、适用性、失效和 Result；
• Observation Ledger：来源、运行、失败、审查和更新观察。

四图分离使多种状态能够同时成立：程序已经完成，候选仍未验证；局部结果已经建立，根问题仍未闭合；某条路线已经失败，其他路线仍可继续。

3. OSPS：F04 结果空间执行面

OSPS（Outcome-Space Parallel Search）是 F04 结果空间执行面。这里的“执行”专指展开、比较和更新 Outcome Space；F05 计算 Job 由过程编排面管理。当前工程实现只承担 candidate planning。

OSPS 负责：

• 归一化根 Outcome；
• 展开候选结果；
• 建立候选关系；
• 去重和识别失败路线；
• 选择有界 frontier；
• 为每条 lane 提出 owner、预算请求和停止条件。

OSPS 不创建 Task、Job、Attempt、EvidenceLink、Result 或 Solution，不启动网页会话、solver、GPU 或证明助手，也不自行传播根闭合。

4. PWTSJ：F05 过程编排面

PWTSJ 的唯一层级是：

Project → Workflow → Task → Step → Job

它把获得授权的候选 lane 转成有界执行。一个 Job 必须具有明确输入、工具、可写范围、时间、内存、输出上限和终止状态。

OSPS 与 PWTSJ 的关系是：

candidate planning
≠ task creation
≠ execution authorization
≠ mathematical admission

5. 不可跨越的状态不变量

Job succeeded
≠ Step accepted
≠ Obligation closed
≠ OutcomeNode closed
≠ Result admitted
≠ Project solved

Issue、聊天、commit、PR、Review、CI、merge 和 checkpoint 都只覆盖各自所在的面。它们提供运输、协作或运行事实；数学 Evidence 仍需独立验证链签发。

四、总体流程：从来源到下一轮搜索

完整循环可以写成：

SourceObservation
  → ProblemContract
  → Outcome Graph
  → bounded Pareto frontier
  → authorization review
  → PWTSJ execution
  → CandidateArtifact
  → adversarial review
  → independent verification
  → EvidenceLink
  → withdrawal decision
     Result | FailedRoute
     Checkpoint | Conflict
  → Outcome Graph update

每轮必须回答三个问题：

1. 本轮试图关闭哪个 Outcome 或 Obligation；
2. 本轮新增了什么可观察信息；
3. 下一轮的搜索空间因此发生了什么变化。

无法回答这三个问题的活动，不应进入长期执行。

五、搜：构造结果空间与搜索前沿

1. 输入冻结

搜索开始前读取 owner truth source，并固定：

• problem_id 与 contract version；
• statement、scope 和 acceptance digest；
• 当前 Obligation、Evidence 和 Result 引用；
• FailedRoute 及其 route signature；
• frontier 上限和预算请求边界。

缺少 active contract、精确摘要或验收谓词时，返回 blocker，不伪造计划。

2. 正交结果坐标

候选 Outcome 至少沿四个维度表达：

• target：根问题、中间数学对象、路线或语义合同；
• effect：建立、反驳、推进、阻塞、修订或独立性；
• output：证明、反例、关系、局部命题、结构、数量、构造/程序、失败知识或语义修订；
• scope：exact、special、conditional、generalized、strengthened、weakened 或 incomparable。

这组坐标避免用单个互相重叠的 family 字段承担全部语义。旧的 resolution、structural、scope、quantitative、constructive、negative knowledge 和 meta 分类，只适合作为派生路由视图。

3. R0–R6 是关闭程度视图

R0–R6 可以帮助阅读 Outcome 离根闭合还有多远：

• R0：探索信息、模式或候选猜想；
• R1：排除路线、技术或辅助引理；
• R2：识别障碍、边界和必要条件；
• R3：建立特殊、局部、条件或有限范围结果；
• R4：建立归约、等价或核心重述；
• R5：完整证明或完整否证根问题；
• R6：进一步得到最优界、完整分类或统一解释。

它是解决程度的派生轴，不参与成果价值排名，也不替代 target、effect、output 和 scope。

4. 九槽搜索投影

为了让网页版 GPT 和其他候选生成器获得互补任务，原子 Outcome 可以投影到九个槽。下表把此前的结果分类讨论与 outcome-space-search Skill 的机器树整理为一个统一视图：

机器分类使用固定的 first-match precedence，表格视觉顺序不参与裁决：

T1 → T2 → T8 → T3 → T5 → T6 → T7 → T4 → T9

在当前机器合同的有限定义域内，5 个 target、7 个 effect 与 9 个 output 形成 315 种组合；验证器要求每种组合按上述优先级唯一落入一个槽。这个结论只说明当前枚举合同内的分类全覆盖，不说明九槽穷尽所有数学成果，更不说明搜索过程完备。七值 scope 仍是正交覆盖轴，不构成第十个槽。

一个原子 Outcome 恰好进入一个槽；复合成果先拆分，再用候选关系连接。T9 是防止新类型和语义缺陷静默丢失的最终 fallback，不证明九槽穷尽数学结果空间。

九槽承担分类投影。网页会话数和并发授权由独立控制面决定。每槽至多产生一个任务候选；槽内子方向保留在同一槽内，不会自动生成额外任务。

5. 候选关系与传播边界

OSPS 可以提出以下候选关系：

depends_on     implies
equivalent_to  refutes
specializes    generalizes
blocked_by     invalidates
supersedes

这些关系必须绑定端点、scope basis 和依据引用，并保持 propagation=none。图连通只说明规划节点没有孤立，不证明蕴含方向、等价关系或反驳关系成立。

6. Route signature 与失败记忆

路线身份不由 route_id 名称决定，而由方法族、表示方式、关键假设、owner、目标 Outcome 和工具能力共同计算 structural route signature。

同一死路改名、换分支或换会话，不能获得“新路线”资格。新的计划必须先读 FailedRoute ledger；历史失败不删除，只能追加、失效或被更强证据 supersede。

7. Pareto 后多样性

每条候选 lane 用公开依据评价：

• root relevance；
• mathematical value；
• semantic clarity；
• verification feasibility；
• information gain；
• route novelty；
• reuse value；
• estimated cost；
• epistemic risk。

这些维度用于选择，不表示命题真值或模型置信度。系统先去掉严格被支配的候选，再在非支配集合中覆盖不同 Outcome、route、representation 和 owner。不能用未披露权重把所有研究价值压成一个神秘总分。

默认 frontier 最多 3 条；机器合同最多保存 9 条，以容纳九槽投影。超过 3 条必须提供绑定输入、资源和预期信息增益的例外说明。

8. 搜的输出合同

一条可交接 lane 至少包含：

lane_id
outcome_id
statement + scope + closure predicate
owner
input references
route signature
requested budget
observable stop condition
expected artifact

requested budget 保持请求状态，获得独立控制面授权后才能执行。OSPS 在生成 candidate plan 后必须停止。

六、打：围绕单一义务执行有界攻防

1. 先授权，再执行

候选 plan 进入独立控制面后，才决定是否创建 Task、Step 和 Job。授权至少检查：

• ProblemContract 和摘要仍然新鲜；
• route signature 没有命中失败路线；
• owner 和工具能力匹配；
• 可写路径、资源和停止条件明确；
• 产物不会越权写入 Evidence 或 Result 真相源。

2. 五步攻防循环

“打”采用有反馈的局部循环：

1. 生成：提出证明、反例、归约、构造、程序或形式化候选；
2. 攻击：检查量词、端点、符号、分支、隐藏假设、定义漂移和已知反例；
3. 修补：把漏洞改写为新 Obligation，只修改受影响节点；
4. 重验：重新执行受影响依赖，不只检查最后一行；
5. 独立验证：核对语义忠实性、适用范围、工具版本、公理和证据能力。

每轮只推进一个可描述的状态变化：关闭一个义务、击破一个候选、排除一条路线、提高一个 scoped Outcome 的证据状态，或确认路线已经停滞。

3. 网页 GPT 与 GitHub 研究渠道

研究渠道采用“网页版 GPT 对话推理 + GitHub 插件受控操作仓库”的模式，在候选分支与门禁范围内完成研究记录、提交、PR 和验证，全程不直接改写数学真相。

预期运输链是：

Issue 绑定 Obligation
  → web/attempt-* 绑定一次候选尝试
  → commit 保存可观察产物
  → PR 展示差异、依据和剩余义务
  → Review 产生攻击与修补项
  → checks 验证格式、路径和可重放性
  → 独立验证链决定 EvidenceLink

网页 GPT 可以生成候选、对抗审稿、局部修补和 ToolPlan；GitHub 保存身份、差异和协作历史。两者都不能给自己的数学主张签发独立 Evidence。

系统只记录可观察输入、候选文件、引用、判据、运行回执和状态变化；隐藏思维链排除在研究产物之外。

4. 工具与证据能力匹配

• 有限枚举只支持声明过的有限范围；
• CAS 只支持对应的符号变换；
• SAT/SMT 结果受编码、理论、solver 和证书约束；
• Lean 内核只检查形式命题和 proof term；
• 模型自评不构成独立验证；
• 测试通过只说明测试覆盖范围内没有发现失败。

工具执行前先定义预期 Evidence capability，执行后再按真实回执登记。不能在看到输出以后反向扩大它的证明范围。

5. 打的停止条件

路线满足任一条件时停止当前 Job 或 lane：

• 目标 Obligation 已由适用证据关闭；
• 候选被反例或语义审查击破；
• route signature 被已知障碍覆盖；
• 预算、时间、内存或产物上限到达；
• 连续有界步骤没有产生新的可检查义务；
• 工具能力与目标不匹配；
• 出现 proof/counterexample conflict。

无限研究由“有界步骤、checkpoint 和换路”组成，不由无 timeout 进程组成。

七、撤：结果准入、失败登记与可恢复停止

1. 撤的五种裁决

准入局部结果：适用证据支持 scoped Outcome，但不传播到更一般根节点。

准入根结果：完整证明或完整反例忠实击中根陈述，并获得适用的独立证据。

登记失败路线：候选或方法被击破，保存 blocker、conclusion、evidence references 和 replacement direction。

保存 checkpoint：路线暂时停滞或预算耗尽，保存 best verified result、next obligation 和重启条件。

冻结冲突：证明与反例同时获得合格支持时，阻断公开导出，审计题面、scope、证明、反例和验证链。

2. Result 的双轴状态

Result 不把成果和证据压成一个等级。

outcome 保存：

undetermined | supported | established
refuted | inconclusive | withdrawn

evidence 分别保存：

numeric_check
symbolic_check
human_review
kernel_check
counterexample_check
axiom_escape_audit
statement_faithfulness
prior_art_review

数值或符号检查只能提供其能力范围内的支持；kernel_check 不替代 statement-faithfulness；自然语言 proof draft 不得标成 kernel-checked。

3. 根闭合条件

根问题只有在适用 Result、语义忠实、独立证据和无冲突同时成立时，才能派生闭合视图：

ProblemContract 继续作为问题身份真相，不另存与 Result 竞争的“已解决状态”。Solution View 只从有效 Result 派生。

4. 撤离必须带走什么

一轮可恢复研究至少保存：

1. 当前 ProblemContract 和摘要；
2. 目标 OutcomeNode、scope 和 closure predicate；
3. Attempt、Route 与 Obligation；
4. CandidateArtifact 及输入、工具和版本；
5. Evidence receipt 与适用性结论；
6. Result、FailedRoute 或 checkpoint；
7. 未闭合义务和唯一下一步入口。

缺少关键对象时，本轮只能记为活动观察，不能承担数学进展声明。

八、动态结果图：把每轮结果带回搜索

结果空间随外部观察更新：

G(next) = Update(
  G(current),
  source review,
  failed routes,
  candidate artifacts,
  evidence,
  results,
  contract version
)

更新规则包括：

• 新来源或语义审查触发 add、split、merge proposal 或 supersession；
• FailedRoute 阻塞相同 route signature，并产生替代路线候选；
• CandidateArtifact 只产生 candidate_found 观察，不关闭节点；
• scoped Result 只更新对应 scope；
• ProblemContract digest 改变后，旧 plan 失去当前适用性；
• 冲突触发证据审计，不选择模型偏好的答案。

历史 plan、FailedRoute 和证据不删除。后续记录通过 supersession 或 invalidation 明确改变当前有效视图。

九、抽象示例：一个全称命题的搜索空间

设根问题为：

结果主导搜索不会只生成“尝试证明”。它可以提出：

• T1：构造覆盖全部 \(X\) 的证明链；
• T2：寻找 \(x_0\in X\) 且 \(\neg P(x_0)\) 的可检查对象；
• T3：把根命题归约为更明确的 \(Q\)；
• T4：证明 \(x\in X_0\subset X\) 时成立；
• T5：刻画最小反例必须满足的结构；
• T6：建立违反 \(P\) 的对象必须满足的定量界；
• T7：构造 witness、certificate 或生成算法；
• T8：证明当前路线依赖的辅助引理不成立；
• T9：发现原题定义、量词或来源版本需要修订。

前沿不会机械取满九条。系统会保留预期信息增益高、验证路径清楚、成本可控且互不重复的少量路线。

不同命中产生不同状态变化：T2 可能形成根否证候选；T8 只淘汰路线；T4 形成 scoped progress；T9 先修订 ProblemContract。分类槽用于保留不同研究价值，Agent 数量由控制面结合预算另行决定。

十、算法化表达与评价指标

1. 规划与执行伪代码

contract = freeze_problem(source)
inputs = read_current_state(contract)

plan = OSPS.expand_and_select(inputs)
validate(plan)
stop_planner()

authorization = control_plane.review(plan)
approved = authorization.approved_lanes
for lane in approved:
    artifact = PWTSJ.execute_bounded(lane)
    critique = adversarial_review(artifact)
    evidence = independent_verify(
        artifact,
        critique
    )
    append_observations(
        artifact,
        critique,
        evidence
    )

recompute_results()
update_outcome_graph()
checkpoint_or_close()

关键分界是 stop_planner()：规划器完成候选前沿后不越权执行。执行器完成 Job 后也不越权准入 Result。

2. 规划质量指标

• Problem/digest binding 正确率；
• duplicate、dangling 和 self relation 拒绝率；
• root propagation 零越权；
• frontier 的 Outcome、route、representation 和 owner 多样性；
• priority basis 完整率；
• repeated failed route 拒绝率；
• requested budget 未授权率；
• downstream handoff 清晰度。

3. 执行质量指标

• 每个闭合 Obligation 的时间和资源成本；
• 可重放执行比例；
• 攻击后仍成立的候选比例；
• checkpoint 可恢复率；
• 重复路线和无边界运行发生率；
• 产物、日志和依赖的可追溯性。

4. 认识论质量指标

• Evidence 与 statement/scope 的适用性；
• 生成者和验证者的独立性；
• statement-faithfulness 覆盖；
• 失效证据是否停止传播；
• 局部结果向根节点越权传播次数；
• public projection 与 internal truth 的一致性。

“生成了多少节点”“开了多少会话”“通过了多少 CI”都不能单独衡量数学研究质量。

十一、与已有 AI for Math 方法的关系

1. FunSearch：generator–evaluator 与程序搜索

FunSearch 将生成代码的语言模型与自动 evaluator 配对，循环选择高分程序、生成变体、执行评价并保留较优候选，同时使用多样性和并行搜索减少停滞。

数学搜打撤吸收生成与评价分离、可执行候选和候选池更新的原则，但不假定每个开放数学问题都有廉价且完备的 evaluator。“程序得分更高”不能自动升级为“数学命题成立”。

2. AlphaEvolve：规模化构造搜索

AlphaEvolve 把 LLM 生成、自动评价和进化搜索用于显式数学构造与定量优化，并明确限定其适用范围，无法覆盖所有数学问题。随机搜索也会增加复现要求。

在搜打撤中，这类方法主要覆盖 T6 定量前沿和 T7 构造前沿。证明、语义修订、方法障碍和题面忠实性仍需要其他 Outcome 和验证能力。

3. Lean 与 Lean Atlas：形式正确和语义忠实

Lean 提供精确表达和内核检查；Lean Atlas 进一步强调，type checker 保证 proof term 对给定形式命题的逻辑正确性，却不保证命题和定义忠实表达原始数学内容。

这正是把 kernel_check 与 statement_faithfulness 分轴记录的原因。形式化构成 AI for Math 的基础，题面审查仍是独立门禁。

4. Lakatos：反例与猜想修订

Lakatos 对局部反例、全局反例、隐藏引理和猜想修订的分析展示了失败的多种状态。反例可能击中根命题，也可能只击中辅助引理；修订可能推进研究，也可能偷偷改变原题。

搜打撤把这些差异落实为 target、scope、relation 和 Result applicability。

5. Terry Tao：可控推进与方法障碍

Terry Tao 对 toy model、特殊情形、obstruction、反例族和 major reduction 的讨论呈现了真实长期研究的常见路径：先获得可控局部结果，再逐步改变问题形状。

搜打撤将这些动作登记为可恢复 Outcome，阶段成果与最终成功证明都进入可追踪记录。

6. 方法定位

OSPS 与 AND/OR graph search、shared blackboard、opportunistic control、HyperTree Proof Search 和 proof dependency graph 相邻，同时保留独立的对象模型与证据边界。

它们提供分解、共享候选、动态调度或证明搜索经验；VibeMath 额外强调 PLFB 身份、scope-aware Outcome、候选关系不传播、失败路线账本、过程授权和证据准入。当前材料不足以主张算法原创优先权、搜索完备性、收敛性或性能最优。

十二、实现状态与信任边界

1. 已公开基础

本文依据公开提交 dea9c5142521db1eb5f76f03b42ecdcb1aecf0be。公开仓库已经提供：

• Point–Line–Face–Body 元模型标准和机器合同；
• Problem、Attempt、Result、Evidence 与研究生命周期边界；
• Formal Methods Map 和可移植验证门；
• 公共问题索引；
• internal 权威源到 public 派生面的单向边界。

2. 已形成的方法实现

结果空间方法已经形成：

• candidate plan schema 与 validator；
• statement/scope canonical digest；
• structural route signature；
• FailedRoute coverage；
• root connectivity 与 typed candidate relations；
• Pareto/frontier 约束；
• T1–T9 九槽投影；
• 合成任务、返回合同和攻击测试。

这些能力仍是 candidate-planning-only，不构成正式 Outcome Graph runtime。

3. 尚未完成

• 正式 Outcome Graph owner ledger；
• PWTSJ identity 与 binding adapter；
• selector runtime 和 orchestrator；
• 真实 Web GPT GitHub connector 的身份与权限闭环；
• 模板和问题仓 fleet rollout；
• 对无限数学结果空间的完备搜索。

当前网页研究渠道的静态合同与合成演练已经建立，但真实 connector 的精确产品身份、installation scope、permission receipt 和无数学业务 smoke 尚未闭合。因此，本文描述的是受控方法和目标架构，不宣称生产级 connector 已全面准入。

4. 明确不作出的主张

本方法不声称：

1. 任意开放问题都能被自动解决；
2. 九槽穷尽全部数学成果；
3. Pareto frontier 是唯一最优选择；
4. 图连通证明数学关系成立；
5. Lean 编译通过自动证明原自然语言命题；
6. 有限计算可以无条件外推到无限范围；
7. 模型自评、PR、CI 或 merge 是数学 Evidence；
8. 当前系统已经产生或准入任何开放问题的完整解。

结语

数学搜打撤把 AI 的长程思考拆成一组可定义结果、可执行义务、可攻击候选、可检查证据和可恢复失败组成的循环。

它的基础是形式化方法、Lean、代码执行和独立验证；它的组织原则是结果主导；它的运行节奏是搜、打、撤；它的真相边界是候选不等于证据、证据不等于 Result、过程完成不等于数学闭合。

当每轮研究都能说明目标、范围、判据、成本、证据和下一步时，AI 的工作才从数学文本生成推进到受控研究。

方法与思想来源

• Lean Programming Language 与 Theorem Proving in Lean 4：Lean 作为开源编程语言和证明助手，以及精确、可验证代码与形式证明的基础。
• Mathematical discoveries from program search with large language models：FunSearch 的 generator–evaluator、程序搜索、多样性与迭代选择。
• FunSearch: Making new discoveries in mathematical sciences using Large Language Models：方法概览与可解释程序输出。
• Mathematical exploration and discovery at scale：AlphaEvolve 的规模化构造搜索、适用范围与复现边界。
• Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization：形式证明正确性与陈述语义忠实性的分离。
• Imre Lakatos: Proofs and Refutations：反例、隐藏引理和猜想修订。
• Be sceptical of your own work：反例搜索、方法障碍和对自身工作的攻击。
• Continually aim just beyond your current range：从可控部分结果逐步扩大研究范围。

公开入口

• 查看本文依据的固定快照
• 查看当前公开仓库
• 阅读点线面体模型 v0.1
• 阅读研究任务全生命周期模型
• 阅读 Formal Methods Map
• 查看 Vibe Mathing 公共问题索引
• 查看公开观察台
• Vibe Mathing 中文社区

Recommended citation: tradecatlabs. (2026). "数学搜打撤：结果主导的 AI for Math 研究搜索法." Public research methodology and infrastructure, snapshot dea9c51.