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, at Kyoto University in Japan 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. Mathematicians 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 on its work that, 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 鈥渓ively discussions鈥�, according to the report, but have yet to land on a conclusive decision on whether IUT theories stand up or not. 鈥淭he members were unable to reach complete consensus on this point,鈥� reads the paper.
They reference a problem they call 鈥渢he wall鈥�, which relates to a flaw in IUT described in 2018 by two prominent mathematicians 鈥撀犅燼t the University of Bonn and聽聽at Goethe University Frankfurt in Germany.聽The report sets out how the problem the pair raised still haunts IUT theory and has rendered it 鈥� so far 鈥� impervious to formalisation.
New 杏吧原创 contacted the five core members of the LANA project, as listed in the report, for comment, but has not yet received a response.
聽at Queen Mary University of London says that the majority of mathematicians see IUT as a flawed theory and the report backs that up. 鈥淢ost people believe that there is a serious gap,鈥� says Saha. 鈥淎nd 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 at the University of York, UK.
But IUT theory still has its cheerleaders who believe a formalised proof will emerge in time.
鈥淧eople followed [Scholze鈥檚] opinion, accepting that it should be the utmost truth,鈥� says at Westlake University in China. 鈥淸But] his take on IUT is totally wrong.鈥�
