Å®ÉúСÊÓƵ

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, at the University of Bath, UK, has turned a formalisation language called Lean towards the field of physics. He attempted to formalise 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.

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.

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.

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 didn’t respond to a request for comment from New Å®ÉúСÊÓƵ, 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.