An effort to verify a controversial proof of the ABC conjecture using computer software has made no progress. An interim report from the Lean and Anabelian Geometry project shows that mathematicians remain divided over the validity of the underlying theory.
In 2012 Shinichi Mochizuki at Kyoto University presented a 500-page proof of the ABC conjecture. The proof relies on his Inter-universal Teichmüller theory, which few mathematicians have been able to verify.
A project known as LANA has attempted to formalise the proof in the Lean programming language. Its recent interim report states that members held lively discussions but failed to reach consensus on whether the theory holds.
The report highlights ongoing issues first raised in 2018 by Peter Scholze and Jakob Stix. Abhishek Saha of Queen Mary University of London said the outcome matches the view of most mathematicians that a serious gap exists in the theory.
Ivan Fesenko at Westlake University maintains that the criticism is misplaced and that a formalised proof will eventually appear.