一種旨在可靠驗證數學定理并找出邏輯缺陷的計算機語言被用于分析一篇物理論文，并發現了一處錯誤。這一發現引發了人們的疑問：還有多少其他論文可能存在類似的問題？

作者：馬修·斯帕克斯

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