全部 · 2026-04-27

Bolzano 在 8 个数学和理论计算机问题上产出新结果，其中 6 个达到可发表研究级别，5 个基本自主完成。我对这篇的判断很直接：它不是又一篇“LLM 能不能证明奥数题”的热闹，而是把数学研究从单轮答案生成，推进到可复用的 agentic research loop。并行 prover、verifier agent、跨轮持久知识库，这三件事组合起来，比单个模型在某个 benchmark 上多拿 3 分更有杀伤力。 这条消息放在 2026 年看，位置很微妙。2023 年大家还在拿 GPT-4 做 IMO shortlist、Lean 形式化题和 miniF2F，主要问题是模型会不会胡编证明。2024 年到 2025 年，DeepMind 的 AlphaGeometry、AlphaProof 路线把“符号系统 + 神经搜索”推得更硬。OpenAI、Anthropic、DeepSeek、Qwen 这些通用模型也在 AIME、MATH、SWE-bench 上持续卷推理。但那些成绩大多还是 benchmark 语境：题目固定、答案已知、评分器清楚。Bolzano 这篇的说法更危险一点：8 个问题里有新结果，6 个够发表，5 个基本自主。研究语境里，评分器没有提前写好，验收靠同行读证明。 我比较在意它的系统形态。并行 prover agent 负责探索多个证明路线，verifier agent 负责筛掉错误，persistent knowledge base 把中间发现带到下一轮。这套设计和过去一年 coding agent 的有效形态很像：不是让一个模型憋出最终答案，而是让多个尝试在状态空间里碰撞，再用验证层收缩搜索。Devin、OpenAI Codex 类产品、Claude Code 这条线都已经证明，长任务能力不是靠“更会说”长出来的，而是靠任务拆分、状态记忆、工具调用和回归检查堆出来的。Bolzano 把同样工程范式搬到数学研究，难点从 CI 测试变成证明审核。 但我不会直接买下“LLM 已经会做数学研究”这个标题感。正文摘要没有披露 8 个问题的完整难度分布，也没有给出每个结果的人类介入分钟数、失败轮数、模型调用成本、使用的底座模型、温度设置、检索语料边界。它引用 Feng 等人的 significance-autonomy taxonomy，说 6 项可发表、5 项基本自主；这个分类很有用，但它不是同行评审本身。数学里“可发表”的跨度太大，从一个组合计数小引理到一个领域核心猜想都能进论文。没有 problem list 和审稿状态，我会把它看成强信号，不会把它看成定案。 这里有个老问题：验证比发现便宜多少。Lean、Coq、Isabelle 这类形式化系统给的是机器可检验路径，但很多数学研究论文仍是自然语言证明。Bolzano 有 verifier agent，不等于有 formal verifier。摘要没有说 8 个结果是否全部形式化，正文片段也没披露验证机制的精确边界。如果 verifier 只是另一个 LLM，那它会降低低级错误率，却不能消除同源幻觉。要是它接了 Lean 或专门的 SAT/SMT/计算验证工具，可信度会明显上一个台阶。这里正文未披露，我不替它补。 外部参照上，我会把它和 Bubeck、Woodruff 那批“AI for math research”报告放一起看。Bubeck 早期材料强调模型的 emergent reasoning，Woodruff 一类工作更贴近理论计算机科学里的辅助发现。Bolzano 的新意在工作流，不在一句“模型变聪明了”。这很像 AlphaGeometry 当时的关键点：不是 Gemini 单独解几何，而是语言模型提供构造，符号引擎负责闭环。数学研究最怕漂亮但漏洞的叙述，agent 系统要活下来，必须把“发现”和“验算”拆成不同角色。 我自己的疑虑还有一个：8 个 case study 容易产生选择偏差。一个开放系统如果跑了 80 个问题，最后写出 8 个成功案例，和一开始挑 8 个问题都成功，含金量差很多。摘要没有披露总尝试池、失败案例、放弃标准和负结果比例。对研究型 agent 来说，失败分布比成功故事更能说明问题。因为数学家真正关心的是：我给它一个陌生 lemma，它平均烧多少 token、多少轮、多少人工提示，能把失败变成有用 conjecture 吗？这部分现在看不到。 即便这样，Bolzano 仍然值得认真对待。原因不是“5/8 自主”这个数字单独很大，而是它贴上了一个可复现实验框架：开源、多 agent、持久知识库、分类标注、33 页论文、项目页公开。如果代码、prompt、问题集和验证记录足够透明，同行可以复跑，也可以专门攻击它的 autonomy claim。数学研究的 AI 化不会先从 Fields Medal 级问题开始，它会先吃掉组合数学、离散优化、理论 CS 里那些局部 lemma、构造例、反例搜索、边界改进。Bolzano 正好打在这个缝上。 我会把这篇放进“研究 agent 从演示走向产出”的文件夹。它离替代数学家还远，离成为数学组里的低成本合作者已经不远。标题已给出 6/8 可发表和 5/8 基本自主，正文摘要没有披露底座模型、成本和形式化验证比例；这三个洞不补上，任何兴奋都要打折。但如果完整 PDF 里的 8 个结果经得住领域专家复核，这篇会比许多刷推理榜的模型发布更有历史感。