一種旨在可靠驗(yàn)證數(shù)學(xué)定理并找出邏輯缺陷的計(jì)算機(jī)語(yǔ)言被用于分析一篇物理論文，并發(fā)現(xiàn)了一處錯(cuò)誤。這一發(fā)現(xiàn)引發(fā)了人們的疑問(wèn)：還有多少其他論文可能存在類似的問(wèn)題？

作者：馬修·斯帕克斯

2026年3月26日

機(jī)器可以幫助發(fā)現(xiàn)數(shù)學(xué)錯(cuò)誤

Alamy Stock Photo

一種用于檢測(cè)數(shù)學(xué)定理錯(cuò)誤的計(jì)算機(jī)語(yǔ)言首次揭示了一篇被廣泛引用的物理論文中的一個(gè)根本性錯(cuò)誤。發(fā)現(xiàn)這一錯(cuò)誤的科研人員表示，這是他首次以這種方式分析物理論文，這也引發(fā)了一個(gè)令人擔(dān)憂的問(wèn)題：還有多少論文存在錯(cuò)誤？

數(shù)學(xué)家們?cè)絹?lái)越多地使用專門(mén)的軟件來(lái)檢查他們的證明是否正確，是否存在矛盾和邏輯漏洞，這個(gè)過(guò)程被稱為形式化。這種方法甚至被認(rèn)為是解決一些最棘手的數(shù)學(xué)問(wèn)題的潛在方案，例如望月伸一長(zhǎng)達(dá)500頁(yè)的ABC猜想證明，專家們多年來(lái)一直對(duì)此爭(zhēng)論不休。

現(xiàn)在，英國(guó)巴斯大學(xué)的約瑟夫·圖比-史密斯（Joseph Tooby-Smith ）將一種名為L(zhǎng)ean的形式化語(yǔ)言應(yīng)用于物理學(xué)領(lǐng)域。他試圖將2006年發(fā)表的關(guān)于雙希格斯雙重態(tài)模型（2HDM）勢(shì)穩(wěn)定性的研究形式化，該研究在之后的幾年里被廣泛引用，但他卻意外地發(fā)現(xiàn)了一個(gè)動(dòng)搖該定理的錯(cuò)誤。

形式化定理可以作為構(gòu)建模塊，用于形式化更復(fù)雜的定理。Tooby-Smith表示，他的工作原本只是一個(gè)“例行公事”，目的是將論文添加到一個(gè)名為PhysLib的大型形式化物理研究項(xiàng)目中。PhysLib的模式借鑒了已建立的數(shù)學(xué)數(shù)據(jù)庫(kù)MathsLib?！拔覀兊哪康牟皇菫榱朔瘩g論文，而是為了構(gòu)建人人都能使用的研究成果，”Tooby-Smith說(shuō)道。

閱讀更多

數(shù)學(xué)正在經(jīng)歷其歷史上最大的變革。

錯(cuò)誤在于原作者的一段陳述，其中提到某個(gè)條件 C 足以保證問(wèn)題的穩(wěn)定解。但 Tooby-Smith 在形式化過(guò)程中證明，存在一個(gè)條件 C 并不能保證問(wèn)題的穩(wěn)定解。

僅限訂閱用戶閱讀的簡(jiǎn)訊

注冊(cè)加入“迷失時(shí)空”

通過(guò)我們每月由特邀嘉賓撰寫(xiě)的簡(jiǎn)報(bào)，解開(kāi)令人費(fèi)解的物理學(xué)、數(shù)學(xué)和現(xiàn)實(shí)的怪誕之處。

訂閱新聞簡(jiǎn)報(bào)

圖比-史密斯表示，這一錯(cuò)誤的發(fā)現(xiàn)具有戲劇性意義。這會(huì)對(duì)論文本身產(chǎn)生影響，但不太可能對(duì)后續(xù)引用和基于該論文的研究造成問(wèn)題。然而，他現(xiàn)在擔(dān)心許多物理學(xué)論文都存在類似的錯(cuò)誤，但并不確定這個(gè)問(wèn)題究竟有多普遍。他認(rèn)為，這有力地證明了形式化應(yīng)該成為發(fā)表新研究的標(biāo)準(zhǔn)流程。

圖比-史密斯表示，物理學(xué)家在定理中往往不像數(shù)學(xué)家那樣給出詳盡的細(xì)節(jié)。“因?yàn)楹芏辔锢韺W(xué)家對(duì)這些細(xì)枝末節(jié)不感興趣，所以他們有時(shí)會(huì)忽略這些細(xì)節(jié)，而這正是錯(cuò)誤產(chǎn)生的原因，”他說(shuō)。

凱文倫敦帝國(guó)理工學(xué)院的巴扎德表示，形式化正在對(duì)數(shù)學(xué)產(chǎn)生巨大影響，而且至少理論物理學(xué)完全可以用同樣的方式來(lái)處理?！拔覀儑L試用這種方式進(jìn)行數(shù)學(xué)研究，結(jié)果發(fā)現(xiàn)非常有趣，”他說(shuō)。

但數(shù)學(xué)形式化的真正益處在于，如今已存在大量形式化定理，這使得數(shù)學(xué)家能夠更容易地在此基礎(chǔ)上進(jìn)行拓展，并訓(xùn)練人工智能模型，從而更快地形式化新的定理。訓(xùn)練這些人工智能模型來(lái)形式化……數(shù)學(xué)需要時(shí)間和大量的具體例子作為訓(xùn)練數(shù)據(jù)，而物理學(xué)可能還沒(méi)有這樣的數(shù)據(jù)。

“理想情況下，我們需要一百萬(wàn)行物理公式，但這可能很難實(shí)現(xiàn)。如果機(jī)器一開(kāi)始在物理運(yùn)算方面表現(xiàn)不佳，那么一開(kāi)始就需要人工干預(yù)，但最終機(jī)器有望接管這項(xiàng)工作，”巴扎德說(shuō)道。

原物理論文的作者沒(méi)有回復(fù)《新科學(xué)家》的置評(píng)請(qǐng)求，但圖比-史密斯表示，他已將自己的發(fā)現(xiàn)告知了他們，并得到了他們同意的確認(rèn)。被告知將會(huì)發(fā)布勘誤表。

參考

arXiv DOI：10.48550/arXiv.2603.08139

主題：

• 數(shù)學(xué)/
• 物理

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