面向数学家的AI智能体

大多数数学家与AI的互动方式相似：向ChatGPT提问，得到类似证明的回应，然后继续工作。这种模式基于一种普遍看法：如果ChatGPT几次尝试未能解决问题，那么AI永远无法独立解决。然而，这种看法是错误的。实际上，有一种更强大的系统——AI智能体——能够以更高的成功率完成数学任务。

AI智能体是能够使用工具的人工智能。这里的工具包括操作系统、Python、LaTeX编译器、SAGE数学软件、浏览器等。智能体可以与环境交互并实际“执行”任务。OpenAI的Codex是一个在本地计算机上运行智能体的编码框架。与普通聊天窗口相比，Codex提供了三大优势：文件作为持久状态（问题陈述、定义、尝试都保存在目录中）、上下文控制（智能体只读取你指定的文件）、工具使用（如Gurobi、SAGE、LEAN等）。此外，智能体可以长时间自主运行，让你离开后回来查看进展或失败记录。

实际使用步骤如下：首先，下载Codex程序并用ChatGPT账户登录，或者直接使用ChatGPT Work。其次，将模型设置为最高可用版本（目前为gpt-5.6-sol ultra）。然后，将精确的数学断言替换到提示词模板中。提示词模板要求创建多个文件来管理状态：STATEMENT.md（精确陈述和成功标准，在整个运行过程中固定不变）、REGISTRY.md（每类方法族的记录，包括族名、尝试的精确断言、剩余缺口、最小的已知障碍、下一个决定性测试和状态）、FAILED.md（所有封闭路线的记录，包括尝试的内容、确切障碍及其证据、以及什么会使重试具有实质性的新内容）、以及PROVED.md（仅记录提升的结果，每个结果带有状态标签和证明或证书）。这些文件成为智能体的记忆，对话内容在上下文压缩后会被丢失，但这些文件会保留。

智能体使用严格的状态词汇来标记每个声明的可靠性：候选（由智能体生成，尚未检查）、自审计（仅由其作者或上下文重新检查）、验证者支持（经过敌对审计和独立重建）、提升（验证者支持并记录在PROVED.md中）、独立审计（由不同模型家族或人类额外检查）。标签只能通过验证步骤提升，且后续论证的确定性不能超过其最弱前提的标签。编排规则要求最多6个并发子智能体，分波次工作：首先采用多样化的方法组合，包括不同的表述、不变量、归约、代数视角、结构归纳、分解、嵌入、极值论证。不要过早透露当前偏好方向，以保持独立性。每条路线结束时需在REGISTRY.md中明确分类为方法失败或反证。每个候选证明需经过一个敌对审计轮次（由另一个智能体试图反驳）和一次独立端到端重构（由未见过证明的智能体基于表述和关键思想进行）。只有通过这两步，标签才提升为验证者支持。最终候选结果还应由不同模型家族进行额外检查。

报告门限要求仅在出现重大更新时汇报：完整的证明或经过认证的反例、移除已命名依赖的已证明引理、关闭路线的极小障碍、或更严格或更简单的带证明定理。新符号、重构、另一个有限计算或归约到定理强度的引理都不算重大。计算规则要求仅在必要时编程，且每次运行需记录来源文件、方法族ID、超时、日志和输出位置。网络政策限制仅用于普通数学背景或标准命名定理，禁止搜索当前问题的解决方案。持续性要求至少运行8小时，只有在完整肯定解通过全部验证后才返回；否则继续维护FAILED.md和REGISTRY.md。

此外，文章还介绍了使用编排器的概念：一个主智能体监督多个子智能体，这比单个智能体更有效，因为后者会快速填满上下文窗口。提示词模板结合了CDC提示词、Danus和个人经验，虽不完美但覆盖了90%的需求。通过这种方法，数学家可以更有效地利用AI解决开放问题，并记录教训以便未来改进。