Mathematicians Attempt to Formalize Controversial ABC Conjecture Proof Using Lean

Background of

the Controversy A proof of the ABC conjecture was announced, introducing new techniques and concepts known as Inter-universal Teichmüller theory (IUT).

Many mathematicians found it difficult to understand, leading to efforts to clarify the work through discussions. Progress stalled after prominent mathematicians identified a possible error in 2018, creating a divide where some maintained the proof's correctness while others viewed it as indecipherable or flawed.

Formalization Projects Underway

Last year, advances in formalization techniques, particularly the Lean language, were highlighted as a way to verify proofs automatically and reduce social influences on mathematical truth.

One project, started late in 2023 at a mathematics center in Japan, enlisted experts familiar with the proof and Lean to settle the controversy. The group reported reaching a deep understanding but became stuck on a point related to the 2018 identified issue. Despite workshops and indirect communications, the team could not advance past this obstacle.

In a press conference last month, project members announced their progress and the specific challenge. A separate group has also begun formalizing the proof in Lean, emphasizing communication over verification, as they consider the proof already correct.

Progress and Outlook

This separate effort targets the controversial section first, producing initial lines of Lean code, though not yet public.

Experts note that fully formalizing such a complex proof will require substantially more code. These developments represent the first significant movement in understanding the proof since its announcement, with ongoing dialogue between groups offering potential for resolution.