A revolutionary computer language has discovered a significant error in a widely cited physics paper for the first time. Researchers highlighted the groundbreaking analysis, raising concerns about the prevalence of errors in academic literature. “How many more publications contain mistakes?” they pondered.

Advanced software is increasingly utilized to help mathematicians validate proofs for accuracy and logical consistency through a method known as formalization. This technique has been suggested as a potential solution to longstanding mathematical conundrums, including Shinichi Mochizuki’s extensive proof of the ABC conjecture.

Recently, Joseph Tooby-Smith from the University of Bath aimed a formalization language called Lean at the realm of physics. In his analysis of a 2006 study on the stability of the two Higgs doublet model (2HDM), which has been extensively referenced, he uncovered an error discrediting the theorem.

Formalizing theorems can act as foundational elements for crafting more intricate mathematical proofs. Tooby-Smith noted that his project was intended to be a simple addition to a comprehensive initiative known as PhysLib, inspired by the established MathsLib database. “We’re not setting out to disprove theories; we aim to create results that everyone can utilize,” he explained.

This error pertained to a claim made by the original author suggesting that a specific condition C would reliably resolve the problem. Yet, Tooby-Smith demonstrated that an alternative condition C fails to yield a stable solution.

While Tooby-Smith acknowledged the serious implications of the discovered error for the paper’s credibility, he indicated it’s improbable that it would significantly impact subsequent studies that referenced it. Nonetheless, he expressed concern over potential similar errors in numerous physics papers, emphasizing the need for formalization to become standard practice in research presentations.

According to Tooby-Smith, physicists often provide less detailed explanations of their theories than mathematicians, which can lead to overlooked errors. “Many physicists are less focused on the fine details; thus, mistakes are more likely to slip through,” he remarked.

Kevin Buzzard, a professor at Imperial College London, affirmed the transformative power of formalization in mathematics and encouraged similar treatment in theoretical physics. “We experimented with this style of mathematics, and it yielded fascinating results,” he stated.

The real advantage of formalization lies in the vast collection of previously formalized theorems, enabling mathematicians to efficiently build upon them and train AI models for quicker theorem formalization. However, gathering the extensive sample data needed for physics might be a considerable challenge.

“Ideally, we would amass a million lines of physics data, but achieving this could be labor-intensive. Initially, the machines may struggle, requiring human intervention, but eventually, automation will prevail,” Buzzard emphasized.

The author of the original physics paper has not yet responded to requests for comments from New Scientist. However, Tooby-Smith reported that he notified them of his findings, received their acknowledgment, and was told that an erratum would be forthcoming.