A specialized computer language, originally designed for verifying mathematical theorems, has identified a significant error within a prominent physics paper for the first time. The researcher responsible for this discovery notes that this is his initial foray into analyzing physics literature using this method, raising concerns about the potential for undetected mistakes in other published works.
The process of formalization, which employs specialized software to ensure mathematical proofs are consistent and free from logical flaws, is becoming increasingly common. This technique has even been proposed as a means to address some of the most challenging problems in mathematics, such as the complex 500-page proof for the ABC conjecture by Shinichi Mochizuki, a subject of extensive debate among experts for years.
Joseph Tooby-Smith, affiliated with the University of Bath, has now applied a formalization language known as Lean to the field of physics. His objective was to formalize research published in 2006 concerning the stability of the two Higgs doublet model (2HDM) potential. This paper, widely referenced since its publication, unexpectedly revealed an error that compromises the validity of its core theorem.
Formalized theorems serve as foundational elements for constructing more intricate proofs. Tooby-Smith indicated that his task was initially intended as a simple verification step, a “tick box exercise” to incorporate the paper into an expansive project on formalized physics research, dubbed PhysLib. This initiative is modeled after MathsLib, an established database for mathematics.
“Our goal isn’t to refute existing papers,” Tooby-Smith stated. “Rather, we aim to construct a body of results that can be reliably used by everyone.”
The identified error pertains to a specific assertion within the original paper. The authors claimed a particular condition, designated as C, was sufficient to ensure a stable solution to the problem. However, Tooby-Smith’s formalization process demonstrated that a condition C exists which, in fact, does not lead to a stable solution.
Tooby-Smith commented that this discovery significantly impacts the original paper, though he anticipates it is unlikely to create downstream issues for subsequent research built upon it. Nevertheless, he expressed concern that numerous physics papers may contain similar errors, without a clear understanding of the problem’s scope. He believes this situation strongly supports the integration of formalization as a standard practice in academic publishing.
According to Tooby-Smith, physicists generally provide less explicit detail in their theorems compared to mathematicians. “Because many physicists are not preoccupied with these fine details, they sometimes overlook them, and that’s how errors can arise,” he explained.
Kevin Buzzard of Imperial College London noted that formalization is already exerting a considerable influence on mathematics. He sees no inherent reason why theoretical physics, at least, could not be subjected to the same rigorous approach. “We attempted this method in mathematics, and it proved to be quite insightful,” Buzzard remarked.
However, the primary advantage of formalization in mathematics currently stems from the substantial collection of pre-formalized theorems. This allows human mathematicians to more easily build upon existing work and facilitates the training of AI models that can expedite the formalization of new theorems. The development of these AI models for mathematics required significant time and a vast quantity of concrete examples for training data, resources that may not yet be readily available for physics.
“Ideally, we would need something on the order of a million lines of physics formalizations, which could be a considerable undertaking,” Buzzard hypothesized. “If the machines are not highly proficient at formalizing physics from the outset, there will be a period of manual effort. Eventually, though, we hope the machines will take over.”
The authors of the original physics paper did not respond to requests for comment. Tooby-Smith did, however, confirm that he had informed them of his findings. He received confirmation of their agreement and was advised that an erratum would be published.