形式化数学：允许探索失败，要求结论可验证
证明搜索与证明检查之间的差异，使数学成为长期 Agent 回路值得关注的方向。但形式正确、命题正确、结果新颖与研究价值，仍是四个不同问题。
值得关注的变化，是把大量不可靠的候选探索连接到严格的结果筛选。这可能改变某些数学问题的求解成本与研究组织方式。
准确性应该放在系统的哪一层
讨论 LLM 的数学能力时，人们常把一次回答是否正确当作全部问题。但研究过程本来就包含大量失败路线。如果系统能够提出候选、得到反馈、保留进展并舍弃错误尝试，那么单次生成不可靠，并不意味着整个工作流没有价值。
我想表达的不是“数学不需要准确性”，而是准确性不必由每一步生成独自承担。探索阶段可以容忍猜错、推导失败与证明策略无效，最终接受结论却必须严格。这与让模型在没有外部检查时直接宣布证明成立，有本质区别。
值得利用的结构是：某些问题的证明搜索非常困难，而给出的形式证明能够被机器检查。这里不存在统一难度倍数，检查也可能昂贵，反例也可能难找。但只要搜索与检查的成本结构适合，增加尝试就可能带来新的有效结果。
Lean 提供强检查，但验收不能只看编译
Lean 由内核检查证明项是否具有声明的类型，证明策略产生的结果仍需经过检查。［1］ ↗ 探索层因而可以使用不同策略和工具，不必将这些工具每一步的推理都作为信任基础。关键是检查目标定理，而不是把项目能够生成可执行程序当作证明完成的判据。
没有 sorry 是必要检查之一，却不是完整验收。Lean 允许声明公理，定理也可能间接依赖其他声明中的占位或不合适假设。官方文档提供公理依赖检查，并说明错误或不一致公理会破坏结论可信性。［2］ ↗ 因而要检查目标定理依赖，固定工具链与库版本，并确认实际构建包含了需要验收的对象。
另一层检查在形式系统之外：代码中的命题是否就是原问题？量词范围是否缩小，前提是否加强，定义是否改变？证明了较弱命题，不等于解决原问题。形式化消除了许多推导歧义，却不会保证翻译过程表达了正确目标。
用 lemma DAG 组织搜索，而不是堆积对话
较长证明可以尝试拆成若干引理，记录各自的命题、依赖与状态。互不依赖的部分允许并行探索，通过检查的结果成为后续推导基础。相比把所有内容放进越来越长的对话，这样更便于定位失败和复用局部进展。
但拆分本身也是需要修正的假设。有些引理过强，有些路径无法组合，还有些依赖只是把原问题换一种表述。系统需要允许重构证明图，区分待证目标和已经成立的结论。节点依赖尚未建立的前提时，不能因为局部文件能够编译就被当作最终成果。
并行价值来自不同搜索路线，而不只是更多执行者。多个 Agent 重复同一个错误分解，可能只会增加成本。调度应记录失败原因、已尝试策略与可复用引理，让新增计算覆盖新的可能性。
生成猜想、寻找反例与证明，是不同阶段
另一条路线是在细分领域生成候选猜想，再通过计算实验和反例搜索筛选。它可以帮助发现模式、排除明显错误，并将人的注意力集中到更值得研究的部分。但“尚未找到反例”必须是独立状态，不能被改写为“猜想成立”。
对于全称命题，一个核实过的反例可以推翻它；找到反例却未必容易。有限搜索只覆盖检查范围，数值实验也受精度与建模影响。把证伪难度固定写成 1，会掩盖这些条件。筛选漏掉的错误候选，仍需进一步证明或更强分析。
通过筛选也不等于具有发表价值。结果可能是已知定理的直接推论，可能用不同记号重复已有工作，也可能正确却无法解释更多现象。生成、反例检验、形式证明、文献核对和价值判断应分开记录，不能用产量替代研究贡献。
已经出现的进展，说明了什么
AI 参与 Erdős 问题求解，已经有可追踪的记录。例如 Erdős Problem #728 有专门整理 Aristotle 形式证明的论文，相关项目也记录了 AI 贡献的案例与结果。［3］ ↗［4］ ↗ 这些材料使讨论可以围绕问题、产物与贡献过程展开，而不必只依赖宣传描述。
陶哲轩在 2026 年 1 月的文章中讨论了精确问题数据库如何使人类、AI 及混合方法系统性推进部分问题，并提出建设优化常数资料库。［5］ ↗ 我得到的启示是：问题整理、明确表述与公共反馈，本身可能成为研究生产力的一部分。这不等于相关人物对职业风险或经费预测已经达成共识。
原创发现、已有结果的重新发现、形式化贡献与人工整理，需要分别判断。与其争论“AI 有没有原创性”的笼统标签，不如检查它究竟贡献了什么：新的结论、新的证明路线，还是将已知论证变成可验证对象。
研究成本的变化，比职业排名更值得跟踪
我的判断是，表述明确、工具能够检查、但过去因投入产出比缺少关注的问题，可能首先受到持续搜索的影响。失败尝试成本下降后，原本没有人愿意长期投入的边缘问题可能进入新的探索范围。这是关于研究经济性的推断，不是保证任何特定问题都能解决。
如果这种变化持续，研究者如何选择问题、组织协作与展示贡献，都可能调整。形式化库、问题资料库与验证基础设施的价值也可能上升。但从技术进步直接推断某国会削减数学经费，或者数学家按固定比例减少，跨越了组织、政策与价值判断等多层不确定性，现有材料不足以支持确定结论。
我更希望观察：在明确任务与预算下，系统能否持续产生经过独立检查的新结果，哪些步骤仍依赖人，新增算力扩大的是有效搜索还是待审查内容。形式化数学的机会，在于让探索更充分，同时让“什么已经成立”更加清楚。