计算机首次发现一篇重要物理学论文中的缺陷

一种旨在可靠验证数学定理并找出逻辑缺陷的计算机语言被用于分析一篇物理论文，并发现了一处错误。这一发现引发了人们的疑问：还有多少其他论文可能存在类似的问题？

作者：马修·斯帕克斯

2026年3月26日

机器可以帮助发现数学错误

Alamy Stock Photo

一种用于检测数学定理错误的计算机语言首次揭示了一篇被广泛引用的物理论文中的一个根本性错误。发现这一错误的科研人员表示，这是他首次以这种方式分析物理论文，这也引发了一个令人担忧的问题：还有多少论文存在错误？

数学家们越来越多地使用专门的软件来检查他们的证明是否正确，是否存在矛盾和逻辑漏洞，这个过程被称为形式化。这种方法甚至被认为是解决一些最棘手的数学问题的潜在方案，例如望月伸一长达500页的ABC猜想证明，专家们多年来一直对此争论不休。

现在，英国巴斯大学的约瑟夫·图比-史密斯（Joseph Tooby-Smith ）将一种名为Lean的形式化语言应用于物理学领域。他试图将2006年发表的关于双希格斯双重态模型（2HDM）势稳定性的研究形式化，该研究在之后的几年里被广泛引用，但他却意外地发现了一个动摇该定理的错误。

形式化定理可以作为构建模块，用于形式化更复杂的定理。Tooby-Smith表示，他的工作原本只是一个“例行公事”，目的是将论文添加到一个名为PhysLib的大型形式化物理研究项目中。PhysLib的模式借鉴了已建立的数学数据库MathsLib。“我们的目的不是为了反驳论文，而是为了构建人人都能使用的研究成果，”Tooby-Smith说道。

阅读更多

数学正在经历其历史上最大的变革。

错误在于原作者的一段陈述，其中提到某个条件 C 足以保证问题的稳定解。但 Tooby-Smith 在形式化过程中证明，存在一个条件 C 并不能保证问题的稳定解。

仅限订阅用户阅读的简讯

注册加入“迷失时空”

通过我们每月由特邀嘉宾撰写的简报，解开令人费解的物理学、数学和现实的怪诞之处。

订阅新闻简报

图比-史密斯表示，这一错误的发现具有戏剧性意义。这会对论文本身产生影响，但不太可能对后续引用和基于该论文的研究造成问题。然而，他现在担心许多物理学论文都存在类似的错误，但并不确定这个问题究竟有多普遍。他认为，这有力地证明了形式化应该成为发表新研究的标准流程。

图比-史密斯表示，物理学家在定理中往往不像数学家那样给出详尽的细节。“因为很多物理学家对这些细枝末节不感兴趣，所以他们有时会忽略这些细节，而这正是错误产生的原因，”他说。

凯文伦敦帝国理工学院的巴扎德表示，形式化正在对数学产生巨大影响，而且至少理论物理学完全可以用同样的方式来处理。“我们尝试用这种方式进行数学研究，结果发现非常有趣，”他说。

但数学形式化的真正益处在于，如今已存在大量形式化定理，这使得数学家能够更容易地在此基础上进行拓展，并训练人工智能模型，从而更快地形式化新的定理。训练这些人工智能模型来形式化……数学需要时间和大量的具体例子作为训练数据，而物理学可能还没有这样的数据。

“理想情况下，我们需要一百万行物理公式，但这可能很难实现。如果机器一开始在物理运算方面表现不佳，那么一开始就需要人工干预，但最终机器有望接管这项工作，”巴扎德说道。

原物理论文的作者没有回复《新科学家》的置评请求，但图比-史密斯表示，他已将自己的发现告知了他们，并得到了他们同意的确认。被告知将会发布勘误表。

参考

arXiv DOI：10.48550/arXiv.2603.08139

主题：

• 数学/
• 物理

Computer finds flaw in major physics paper for first time

A computer language designed to robustly verify mathematical theorems and expose logical flaws has been turned towards a physics paper – and spotted an error. The discovery raises questions about how many other papers may harbour similar issues

By Matthew Sparkes

26 March 2026

Machines can help spot mathematical errors

Alamy Stock Photo

A computer language created to spot errors in mathematical theorems has uncovered a fundamental error in a widely cited physics paper for the first time. The researcher behind the discovery says it is the first physics paper he has analysed in this way, which raises a worrying question: how many more contain mistakes?

Specialised software is increasingly used to help mathematicians check their proofs are correct and free of contradictions and logical holes, using a process known as formalisation. The approach has even been proffered as a potential solution to some of the thorniest problems in mathematics, such as Shinichi Mochizuki’s sprawling, 500-page proof for the ABC conjecture, which experts have quibbled over for years.

Now, Joseph Tooby-Smith at the University of Bath, UK, has turned a formalisation language called Lean towards the field of physics. He attempted to formalise research published in 2006 on the stability of the two Higgs doublet model (2HDM) potential, which has been widely cited in the years since, but accidentally revealed an error that undermines the theorem.

Advertisement

Formalised theorems can be used as building blocks to formalise more complex theorems, and Tooby-Smith says that his work was supposed to be a “tick box exercise” to add the paper to a larger project of formalised physics research called PhysLib, modelled on an established database for mathematics called MathsLib. “We’re not going out there to disprove papers; we’re going out there to build results that everyone can use,” says Tooby-Smith.

Read more

Mathematics is undergoing the biggest change in its history

The error relates to a statement in which the original authors say that a certain condition, C, is sufficient for a stable solution to the problem. But Tooby-Smith showed during formalisation that there is a condition C that doesn’t provide a stable solution.

Subscriber-only newsletter

Sign up to Lost in Space-Time

Untangle mind-bending physics, maths and the weirdness of reality with our monthly, special-guest-written newsletter.

Sign up to newsletter

Tooby-Smith says that the discovery of the error has a dramatic effect on the paper, but is unlikely to cause problems downstream in work that has built on it and cited it. However, he now fears that many physics papers harbour similar mistakes, but isn’t certain how wide-ranging the problem might be. He thinks this makes a strong case for formalisation to become a standard part of publishing new research.

Tooby-Smith says that physicists tend not to give as much explicit detail in theorems as mathematicians. “Because a lot of physicists aren’t interested in these nitty-gritty details, sometimes they miss them, and that’s where you get an error,” he says.

Kevin Buzzard at Imperial College London says that formalisation is having a big impact on mathematics, and that there is no reason that theoretical physics, at least, can’t be treated in the same way. “We tried to do maths like this, and it turned out to be really interesting,” he says.

But the real benefit of formalisation in maths is now coming from the large corpus of existing formalised theorems, which allows human mathematicians to more readily build on top of them and also to train AI models that can help formalise new theorems faster. Training those AI models to formalise mathematics took time and lots of concrete examples to use as training data, which might not yet be available for physics.

“Ideally, we need a million lines of physics, and that might be hard work to get. If the machines aren’t pretty good at doing physics initially, then there’ll be manual work at the beginning, and then eventually the machines will hopefully take over,” says Buzzard.

The authors of the original physics paper didn’t respond to a request for comment from New Scientist, but Tooby-Smith says that he informed them of his discovery, received confirmation that they agreed and was told that an erratum would be published.

Reference

arXiv DOI: 10.48550/arXiv.2603.08139

Topics:

• Mathematics /

• Physics