# 普林斯顿用 DeepSeek V4 做数学证明，成本只要别人的五百分之一

> 原标题：DeepSeek V4做数学证明，500倍成本优势：智能体系统刷新多项纪录

- 来源：机器之心 · 公众号
- 发布时间：2026-06-06T04:00:00.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/34969
- 原文：https://mp.weixin.qq.com/s?__biz=MzA3MzI4MjgzMw==&mid=2651037518&idx=2&sn=2d6012bcb8a495b818fce4458626480d

## 摘要

普林斯顿的研究员搞了一套叫 Goedel-Architect 的智能体系统，专门让模型在 Lean 这种形式化证明语言里自动做数学题。他们拿 DeepSeek-V4-Flash 跑 PutnamBench 数学竞赛题，672 道题里正确率到了 75.6%，API 调用费总共才花了 294 美元。对比之前 Hilbert 系统用别的模型达到 70.0% ...

## 推荐理由

普林斯顿团队搞了个叫Goedel-Architect的智能体系统，让DeepSeek-V4-Flash在形式化证明语言Lean里自动做数学题。PutnamBench 672道题正确率75.6%，API调用费总共294美元，对比之前Hilbert系统用别的模型达到70.0%却花了约17万美元，成本差了近500倍。这个对比很直观，数字也扎实，但正文没详细拆解294美元是怎么算出来的，也没说Hilbert那17万是不是包含了大量试错和人工调参。所以“500倍”这个说法可以先打个折看，不过即使有水分，成本优势依然明显。整体还是偏学术研究，离工程落地有距离，...

## 锐评

这条消息最值得点开的地方是成本：294美元跑完672道PutnamBench数学竞赛题，正确率75.6%，比之前Hilbert系统用别的模型烧掉约17万美元才做到70%正确率，确实省了差不多500倍。系统叫Goedel-Architect，是一个让模型在Lean这种形式化证明语言里自动做题的智能体框架，相当于给模型配了一套在严格数学环境里干活的工作流。

不过现在能看到的只有摘要，原文被微信验证页挡住了，具体怎么设计的智能体、用了什么搜索或验证策略、有没有人工筛选，这些关键细节都看不到。另外，PutnamBench虽然难，但形式化证明和实际数学研究之间还有距离，这个75.6%能迁移到开放问题上的程度还不清楚。

我会先打个折：成本数字确实亮眼，但等看到完整论文再判断这套方法是不是真的普适，还是只在特定题型上省钱。