内容来源：https://www.sciencenews.org/article/math-human-ai-age

内容总结：

当人工智能公司更看重竞争而非合作，我们可能失去对数学的理解。

“呈指数级爆炸式增长，”数学家托马斯·布卢姆在电话中这样向我描述他所在领域涌现的新成果。他当时并不知道，几小时后，OpenAI将发布722份由一款未公开AI模型生成的数学手稿。

这批海量新作让一个问题变得更加紧迫：AI正在如何改变数学发现？在争夺引人注目突破的竞赛中，AI公司通常不公开其方法和数据。这种竞争正在威胁人类协作与理解。

这种张力在布卢姆运营的一个网站上以缩影形式上演。该网站追踪由20世纪最高产数学家之一保罗·埃尔德什提出和收集的1000多个问题的进展。过去，人们在这里协作讨论未解问题——即尚未找到最佳解法、或更广泛数学界尚不知晓解法的问题。但如今，越来越多访客争相用AI证明来关闭这些问题，而他们往往并不理解这些证明。作为英国曼彻斯特大学的数学家，布卢姆不想把时间花在评审AI生成的工作上。因此，在我们通话后不久、在他得知OpenAI将宣布最新结果之前，布卢姆发帖表示他将不再标注问题为“未解”或“已解”，并关闭了评论区。

AI能如此迅速地解决这么多未解问题，确实令人兴奋。但它能帮助数学家理解答案并在此基础上继续推进吗？

OpenAI成果洪流发布仅两天后，谷歌DeepMind一项研究的同行评审版本公之于众。该研究此前今年早些时候以预印本形式首次报道，提供了一个AI系统如何处理未解数学问题的内部视角。研究人员10月8日在《科学》杂志上报告，这个名为AlphaProof Nexus的系统解决了9个埃尔德什问题，并取得了其他多项有趣的数学进展。

报告详细描述了结果的获取方式。此外，人类数学家审核了许多证明。布卢姆说，这与OpenAI和Anthropic处理其数学结果的方式“相当不同”。

研究合著者、伦敦谷歌DeepMind研究科学家斯瓦拉特·乔杜里表示，“任何数学研究AI的终极目标”都应该是“推动由人类数学家所做的数学研究向前发展”。

一窥AI数学机器内部

在这项最近发表的研究中，乔杜里及其同事测试了系统的不同配置。为处理353个未解埃尔德什问题的集合，他们使用了多个由Gemini语言模型驱动的智能体。这些智能体可以调用AlphaProof——一个专门训练来做数学的AI模型，也是整个系统名称的灵感来源——来处理困难步骤。这些智能体还依赖Lean——一种能识别尚未证明步骤的数学软件——来检查其逻辑。智能体共享工作成果，传阅有希望的证明尝试，并丢弃进展不顺的方案。

团队还在完整系统解决的9个问题上测试了一种更简单的设置。独立的Gemini智能体利用Lean的反馈完成证明，不共享尝试也不咨询AlphaProof。这种设置也解决了全部9个问题。在简单问题上，它比完整系统更便宜——使用更少计算资源；在两个最难问题上则更昂贵。团队未确定这种简单设置是否能解决完整系统遗漏的任何问题。

更简单设置能解决与完整系统相同的9个问题，这令乔杜里感到惊讶。这表明，能力日益增强的语言模型可以借助相对简单的检查工具来攻克研究级数学。

但计算机检查有一个前提。Lean只检查其收到的陈述，即按代码所写的内容。而数学陈述在翻译为Lean代码或从Lean代码翻译回来时，可能出现错误。10月6日的一份预印本说明了这种翻译为何重要。在该论文中，研究人员指出了OpenAI所写纳维-斯托克斯证明与其Lean版本之间的不匹配之处。团队写道，这些不匹配并不意味着书面证明有误，但他们指出，有效的Lean证明并不自动验证AI生成的数学论文。

这就是人类数学家为DeepMind发表成果所做审核如此重要的原因。“人类数学家必须真正思考问题，并为系统设定目标，”乔杜里说。即使系统未能完成证明，其经过检查的步骤也能帮助数学家聚焦于剩余缺口。“数学归根结底是一门人类艺术，”乔杜里说。“系统增强了人类用户的洞察力，人类用户则能用新想法引导系统。”

数学能力伴随责任

AlphaProof Nexus系统取得的数学成果“并非真正处于最重要级别”，未参与该工作的布卢姆说。但这恰恰凸显了团队更为审慎的做法。他说，谷歌DeepMind“试图在科学上更负责任”，而OpenAI等公司则用数学来展示其软件。OpenAI的论文及随附Lean证明完全由AI生成，留给数学界去分辨哪些有用、哪些无用。

OpenAI表示，他们与一个独立顾问小组合作，制定了分享AI数学结果的最佳实践。但该小组表示，他们的建议是不要用未公开的AI模型测试高等数学——该公司显然无视了这一指导。

该公司快速、竞争性的做法继续疏远西北大学的布丽娜·克拉等数学家。她说，公司在引用过往文献方面有所改进。她对AI解决数学重要问题的潜力感到兴奋。但她说，人们普遍担心AI模型获取了他人未发表的工作。“我们曾有一种健康、协作、共享的文化，如今正被摧毁，”她说。“现在，人们对分享想法心存戒备。”

并非所有数学家都如此看待AI。这项技术“让数学更易触及”，安德鲁·特纳说。他质疑为何应由一小群数学家决定我们如何解决问题。特纳曾学习数学和物理，现在是总部位于纽约的Plasma AI公司首席技术官。他认为“数学正在变成工程学”。用机器做数学将让人们能够“回答此前无法想象的问题”。

布卢姆关闭其网站上的竞赛几天后，Plasma AI宣布了一个追踪埃尔德什问题进展的新网站。他们将欢迎AI成果。

布卢姆不把数学视为硅谷式的“快速行动、打破常规”竞赛。我同意，并希望有好奇心的人继续探索他们关心的问题，让AI帮助而非接管。在宣布网站变更的帖子结尾，布卢姆写了一段让我每次读都热泪盈眶的话。我希望每个人，即使是最热情的AI用户，都能为这类工作腾出时间：“困惑吧，卡住吧，受启发吧。找到一个凌乱的证明，再找一个更好的，”他写道。“累了，饿了，进入心流状态。争论，大笑，放弃，喝点咖啡，再攻一次。做个人。让你的大脑敞开着。”

中文翻译：

在人工智能时代，数学还能保持人性吗？
当AI公司重竞争而轻合作，我们可能错失真正的理解

“呈指数级爆炸式增长，”数学家托马斯·布鲁姆在电话里这样向我形容他所在领域涌现的新成果。他当时并不知道，几小时后，OpenAI将发布722份由一款未公开的AI模型生成的数学手稿。

这股新成果的洪流让一个问题变得更加紧迫：AI正在如何改变数学发现？在争相追逐引人注目的突破的过程中，AI公司通常不会公开其方法和数据。AI公司之间的这种竞争，有可能压倒人类之间的协作与理解。

这种张力一直在布鲁姆运营的一个网站上以微缩的形式上演。该网站追踪1000多个问题的进展，这些问题最初由保罗·埃尔德什提出并收集，他是20世纪最多产的数学家之一。在这里，人们过去常常协作讨论未解问题，即那些尚未找到最佳解法、或更广泛的数学界尚不知晓解法的问题。但越来越多的访客开始争相用AI证明来攻克这些未解问题，而这些证明他们往往自己都看不懂。布鲁姆是英国曼彻斯特大学的数学家，他不想把自己的时间花在审阅AI生成的工作上。因此，在我们通话后不久，在他得知OpenAI即将公布最新成果之前，布鲁姆发帖表示他将不再标注问题为“未解”或“已解”，同时也关闭了评论区。

AI能够如此迅速地攻克如此多的未解问题，这无疑令人兴奋。但它能帮助数学家理解这些答案并在此基础上继续推进吗？

就在OpenAI大量发布成果仅仅两天后，谷歌DeepMind一项研究的同行评审版本公开了。该研究今年早些时候曾以预印本形式首次报道，它提供了一个AI系统如何攻克未解数学问题的内部视角。研究人员在10月8日的《科学》杂志上报告称，这个名为AlphaProof Nexus的系统解决了9个埃尔德什问题，并取得了若干其他有趣的数学进展。

该报告详细描述了这些结果是如何获得的。此外，人类数学家对许多证明进行了审核。布鲁姆说，这与OpenAI和Anthropic处理其数学成果的方式“截然不同”。

该研究的合著者、伦敦谷歌DeepMind的研究科学家斯瓦拉特·乔杜里表示，“任何数学AI研究的终极目标”，应当是“推动由人类数学家所做的那种数学研究向前发展”。

一窥AI数学机器的内部

在最近发表的这项研究中，乔杜里及其同事测试了他们系统的不同配置。为了攻克353个未解埃尔德什问题，他们使用了多个由Gemini语言模型驱动的智能体。这些智能体可以调用AlphaProof——一个专门训练来做数学的AI模型，也是整个系统名称的灵感来源——来处理困难步骤。这些智能体还依赖Lean——一种能识别尚未被证明步骤的数学软件——来检查其逻辑。智能体之间共享工作成果，传阅有希望的证明尝试，并丢弃进展不顺的方案。

团队还在完整系统所解决的那9个问题上测试了一种更简单的配置。独立的Gemini智能体利用Lean的反馈来完成证明，不共享尝试，也不咨询AlphaProof。这种配置同样解决了全部9个问题。在简单问题上，它比完整系统更便宜——使用更少的计算资源——而在两个最难的问题上则更昂贵。团队未能确定这种更简单的配置是否能解决完整系统所遗漏的任何问题。

令乔杜里感到意外的是，更简单的配置竟然能解决与完整系统相同的9个问题。这表明，能力日益强大的语言模型可以借助相对简单的检查工具来攻克研究级数学问题。

但计算机检查有一个前提条件。Lean只检查它所收到的陈述，即按其代码所写的内容。而一个数学陈述在翻译为Lean代码或从Lean代码翻译回来时，可能出现错误。10月6日的一篇预印本论文说明了这种翻译为何重要。在该论文中，研究人员指出了OpenAI所写的纳维-斯托克斯方程证明的某些部分与其Lean版本之间的不匹配。团队写道，这些不匹配并不意味着书面证明是错误的，但他们指出，一个有效的Lean证明并不能自动验证一篇AI生成的数学论文。

这就是为什么人类数学家为DeepMind这篇论文所做的审核如此重要。乔杜里说：“人类数学家必须真正深入思考问题，并为系统设定目标。”即使系统未能完成某个证明，其经过检查的步骤也能帮助数学家聚焦于剩余的缺口。乔杜里说：“数学归根结底是一门人类艺术。该系统增强了人类用户的洞见，而人类用户则能够用新想法引导系统。”

数学能力越大，责任越大

布鲁姆并未参与这项工作，他说AlphaProof Nexus系统所取得的数学成果“并非真正处于最重要的层级”。但这恰恰凸显了该团队更为审慎的做法。他说，谷歌DeepMind“试图在科学上更加负责任”，而像OpenAI这样的公司则在利用数学来展示其软件。OpenAI的论文及随附的Lean证明完全由AI生成，留给数学界自己去分辨哪些有用、哪些无用。

OpenAI表示，他们与一个独立咨询小组合作，制定了关于如何分享其AI数学成果的最佳实践。但该小组表示，他们的建议是不要在高级数学上测试未发布的AI模型——而该公司显然无视了这一指导。

该公司这种快速推进、竞争导向的做法，持续让一些数学家和机构感到疏远，其中包括伊利诺伊州埃文斯顿西北大学的布丽娜·克拉。她说，该公司在引用过往文献方面做出了一些改进。她对AI解决数学重要问题的潜力感到兴奋。但她说，人们普遍担忧AI模型获取了他人未发表的研究成果。“我们曾经有一种健康、协作、共享的文化，而这种文化正在被摧毁，”她说，“现在，人们对自己想法的分享变得小心翼翼。”

并非所有数学家都对AI持这种看法。这项技术“正在让数学变得更易触及”，安德鲁·特纳说，他质疑为什么应由一小群数学家来决定我们该如何解决问题。特纳曾学习数学和物理，现在是总部位于纽约的公司Plasma AI的首席技术官。他认为“数学正在变成工程学”。用机器做数学将让人们能够“回答此前无法想象的问题”。

在布鲁姆关闭其网站上的竞争几天后，Plasma AI宣布了一个追踪埃尔德什问题进展的新网站。他们将欢迎AI成果。

布鲁姆不认为数学应该是一场硅谷式的“快速行动、打破常规”的竞争。我同意，并希望充满好奇心的人们继续探索他们关心的问题，让AI提供帮助而非取而代之。在宣布其网站变更的帖子末尾，布鲁姆写了一段话，我每次读到都会热泪盈眶。我希望每个人，即使是最热衷AI的用户，都能为这类工作留出时间：“去困惑，去卡住，去被启发。找到一个凌乱的证明，然后找到一个更好的，”他写道，“累了，饿了，进入心流状态。争论，大笑，放弃，喝杯咖啡，再次发起冲击。做人。让你的大脑保持开放。”

英文来源：

Can math stay human in the age of AI?
When AI companies value competition over collaboration, we may lose out on understanding
“Exponentially exploding,” mathematician Thomas Bloom told me by phone, describing the flood of new results in his field. Little did he know that hours later, OpenAI was going to post 722 mathematical manuscripts an unreleased AI model had produced.
The firehose of new work lends new urgency to the question: How is AI changing mathematical discovery? In their race for headline-grabbing breakthroughs, AI companies typically do not disclose their methods and data. That competition among AI companies threatens to overwhelm human collaboration and understanding.
This tension had been playing out in miniature on a website Bloom runs that tracks progress on more than 1,000 problems originally posed and collected by Paul Erdős, one of the 20th century’s most prolific mathematicians. Here, people used to collaborate to discuss open problems, or ones for which the best solution either hasn’t been found or isn’t known to the greater math community. But increasingly, visitors were competing to close open problems with AI proofs that they often didn’t understand. Bloom, a mathematician at the University of Manchester in England, doesn’t want to spend his days refereeing AI-generated work. So, soon after we spoke, and before he knew that OpenAI would be announcing its latest results, Bloom posted that he’d no longer tag problems as open or solved, and he also closed comments.
It’s definitely exciting that AI can tackle so many open problems so quickly. But can it help mathematicians understand the answers and build on them?
Just two days after OpenAI’s deluge of results, the peer-reviewed edition of a Google DeepMind study became public. First reported in a preprint earlier this year, it offers an inside look at how one AI system tackles open math problems. The system called AlphaProof Nexus solved 9 Erdős problems and made a number of other interesting mathematical advances, researchers report October 8 in Science.
The report includes a detailed description of how the results were obtained. Plus, human mathematicians vetted many of the proofs. That’s “quite different” from how OpenAI and Anthropic are handling their math results, Bloom says.
“The ultimate objective of any AI for math research,” says research scientist and study co-author Swarat Chaudhuri of Google DeepMind in London, should be “to advance mathematics as done by human mathematicians.”
A look inside an AI math machine
In the recently published study Chaudhuri and his colleagues tested different configurations of their system. To tackle a collection of 353 open Erdős problems, they used multiple agents powered by the Gemini language model. These could call on AlphaProof, an AI model specially trained to do math, and the inspiration for the name of the overall system, for difficult steps. The agents also relied on Lean, math software that identifies steps that remain unproven, to check their logic. The agents shared their work, circulating promising proof attempts and discarding ones that weren’t going well.
The team also tested a simpler setup on the nine problems the full system solved. Independent Gemini agents worked through proofs using Lean’s feedback, without sharing attempts or consulting AlphaProof. That setup solved all nine, too. It was cheaper—using fewer computing resources—than the full system on easy problems and more expensive on the two toughest ones. The team did not establish whether the simpler setup would solve any of the problems the full system had missed.
The fact that the simpler setup could solve the same nine problems as the full system surprised Chaudhuri. It suggests that increasingly capable language models can tackle research mathematics with relatively simple checking tools.
But computer-checking comes with a caveat. Lean checks only the statement it’s given, as it is written in its code. And a mathematical statement may be incorrectly translated to or from Lean code. An October 6 preprint shows why this translation matters. In the paper, the researchers pinpoint mismatches between parts of OpenAI’s written Navier–Stokes proof and its Lean counterpart. The mismatches do not mean the written proof is wrong, the team writes, but they note that a valid Lean proof does not automatically validate an AI-generated math paper.
That’s why the vetting human mathematicians did for the DeepMind publication is so important. “The human mathematician has to really think through the problem and set goals for the system,” Chaudhuri says. And even if the system failed to finish a proof, its checked steps helped mathematicians focus on the remaining gaps. “Math is ultimately a human art,” Chaudhuri says. “The system enhances the human user’s insights, and the human user is able to guide the system with new ideas.”
With math ability comes responsibility
The mathematical results that the AlphaProof Nexus system achieved are “not really at the top level of importance,” says Bloom, who wasn’t involved with the work. But that underscores the team’s more measured approach. Google DeepMind, he says, is “trying to be more responsible with the science,” while companies like OpenAI are using math to showcase their software. OpenAI’s papers and accompanying Lean proofs were entirely AI-generated, leaving it up to the math community to work out what’s useful or useless.
OpenAI says they worked with an independent advisory group to develop best practices on how to share their AI math results. But that group has said their advice was to not test unreleased AI models on advanced math, guidance the company clearly ignored.
The company’s fast-moving, competitive approach continues to alienate mathematicians such as Bryna Kra of Northwestern University in Evanston, Ill. She says the company made some improvements in their efforts to cite past literature. And she’s excited about AI’s potential to solve important problems in math. But there is widespread concern, she says, that AI models have accessed people’s unpublished work. “We had a healthy, collaborative, sharing culture that is being destroyed,” she says. “Now, people are wary of sharing their ideas.”
Not all mathematicians feel this way about AI. The technology is “making math more accessible,” says Andrew Turner, who wonders why a small group of mathematicians should get to decide how we solve problems. Turner, who studied math and physics and is Now CTO of the company Plasma AI, based in New York City thinks “math is becoming engineering.” And doing math with machines will allow people to “answer questions previously unfathomable.”
A few days after Bloom shut down the competition on his website, Plasma AI announced a new website to track progress on Erdős problems. They will welcome AI results.
Bloom doesn’t see math as a Silicon Valley–esque move-fast-and-break-things competition. I agree, and hope that curious people will continue to explore problems they care about, with AI helping rather than taking over. At the end of his post announcing the changes to his website, Bloom wrote something that makes me tear up every time I read it. I hope everyone, even the most enthusiastic AI users, can find the time for this type of work: “Be confused, be stuck, be inspired. Find a messy proof, then find a better one,” he wrote. “Get tired, get hungry, get into a flow state. Argue, laugh, give up, drink some coffee and attack it again. Be human. Let your brain be open.”