Effort to solve biggest controversy in mathematics has made no progress

An attempt to bring unequivocal clarity to one of the most controversial areas of mathematics has so far come to nothing. Mathematicians have been working on using a computer to check an apparent proof of the ABC conjecture, but an interim report says there are still serious barriers to overcome. In 2012, Shinichi Mochizuki at Kyoto University surprised the world with his 500-page proof of the ABC conjecture, a deceptively simple conjecture about the equation a + b = c and how the numbers involved can be split up into smaller prime numbers. Mathematicans had struggled to find a proof for decades before Mochizuki came along. The problem was, few could actually understand and therefore verify his proof, which hinges on an entirely new field of mathematics that Mochizuki created called Inter-universal Teichmüller (IUT) theory. As a result there is a small group of people who vehemently believe the proof is sound but others remain unconvinced. Advertisement However, one thing that both sides agree on is that computer formalisation could solve the issue. This involves using software – in this case a programming language called Lean – to represent mathematical arguments in code. A computer can then check if the entire proof is correct. Two projects sprung up to do this: one run by Mochizuki himself, and one run by ZEN Mathematics Center in Japan called the Lean and Anabelian geometry (LANA) project. LANA has now published an interim report on its work which, far from setting out a formalised proof of what Mochizuki has been trying to explain to the world for over a decade, seems to have become bogged down in the problem. LANA members have had “lively discussions”, according to the report, but have yet to land on a conclusive decision on whether IUT theories stand up or not. “The members were unable to reach complete consensus on this point,” reads the paper. They reference a problemn they call “the wall” which relates to a flaw in IUT described in 2018 by two prominent mathematicians – Peter Scholze at the University of Bonn and Jakob Stix at Goethe University Frankfurt. The report sets out how the problem the pair raised still haunts IUT theory and has rendered it – so far – impervious to formalisation. New Scientist contacted the five core members of the LANA project, as listed in the report, for comment but has not yet received a response. Abhishek Saha at Queen Mary University of London says that the majority of mathematicians see IUT as a flawed theory and the report backs that up. “Most people believe that there is a serious gap,” says Saha. “And I think that this particular report is fully consistent with that: it has not managed to formalise it, which is what we would expect if this big theory had some serious gaps.” A large amount of maths has already been built on top of IUT theory, which would be in jeopardy if it is proved incorrect, but that indeed most mathematicians believe it will be, says Chris Bowman-Scargill at the University of York says. But IUT theory still has its cheerleaders who believe a formalised proof will emerge in time. “People followed [Scholze’s] opinion, accepting that it should be the utmost truth, says Ivan Fesenko at Westlake University. “[But] his take on IUT it totally wrong.”