Can a computer program resolve mathematics' most bitter dispute?
In 2012, Shinichi Mochizuki claimed to have proven the ABC conjecture, but his 500-page proof sparked a decade of intense controversy. This video explores the mathematical impasse and the new attempt to use computer formalisation to find the truth.
The dispute centers on the ABC conjecture, a problem involving the relationship between prime numbers in the equation a + b = c. Mochizuki introduced Inter-universal Teichmüller theory (IUT) to solve it, but the complexity of these new techniques left much of the mathematical community unable to verify the work. In 2018, mathematicians Peter Scholze and Jakob Stix identified what they believed to be a potential error, leading to a stalemate between Mochizuki's supporters and his critics.
To break this deadlock, researchers are turning to formalisation—translating proofs into computer languages like Lean to allow for automatic verification. Projects like the Lean and Anabelian geometry (LANA) project, launched by Kato Fumiharu in late 2023, aim to settle the controversy. While progress is being made, experts like Adam Topaz note that researchers have hit a roadblock when trying to understand a specific point within the IUT framework.
Source: The Most Controversial Idea In Math
