用AI辅助攻克数学开放题：长程搜索与对抗审查流程公开

开发者 @FinanceYF5 详细分享了利用 AI 辅助解决数学开放问题的完整流程，并公开了相关证明与提示词。该实践表明，通过合理的任务拆解与模型调度，AI 能够在复杂的数学证明中发挥实质性作用。

已确认

该流程的成功依赖于三个核心环节。首先是**选题**，开发者优先选择数学家（如 Terence Tao）正在关注的问题，并利用 AI 过滤掉难度过高或与重大未解猜想强绑定的题目。其次是**提示词构造**，借鉴 OpenAI 解决 cycle double cover conjecture 时的模板，要求系统首先精确定义“什么才是真正解决该问题”，并列出较弱的无效结果与特定陷阱。最后是**模型选择与执行**，开发者使用 GPT-5.6 Sol 并开启 Ultra reasoning effort，将提示词直接粘贴进 Codex 让其自主运行。部分问题耗时约 6 小时得出解法，另一些则长达 32 小时。

在证明过程中，系统被要求执行严密的**对抗性审查**。它会并行保留多条互不兼容的证明路线，主动寻找反例，并指派独立的对抗性 Agent 攻击候选论证。若某条路线只是将原问题转化为同等难度的未证命题，则会被标记为 blocked。系统会在此循环中不断自我质疑，直到找不到实质性漏洞。

目前，开发者已在公开仓库中放出了每个问题的证明 PDF、LaTeX 源文件和对应提示词。部分问题附带用于计算实验的 Python 文件，其中两个问题已完成 Lean 形式化证明，其余形式化工作仍在推进中。

为什么重要

该实践展示了大语言模型在处理长程、严谨的数学搜索任务时的潜力。通过结合强大的底层模型（GPT-5.6 Sol）、超长的工作时间（最高 32 小时）以及结构化的对抗审查提示词，AI 能够自主完成复杂的逻辑推演与自我纠错，为高难度学术研究提供了新的自动化范式。

2026-07-26 ~ 2026-07-26 · 8 条相关

一手来源