Una disputa de una década en matemáticas sobre la prueba de la conjetura ABC de Shinichi Mochizuki podría resolverse mediante formalización computacional. Mochizuki ha sugerido traducir su obra de 500 páginas al lenguaje de programación Lean para verificación automatizada. Este enfoque podría tender puentes entre los bandos en conflicto en la comunidad matemática.
La controversia se remonta a 2012, cuando Shinichi Mochizuki, profesor de la Universidad de Kioto en Japón, publicó una extensa prueba de 500 páginas para la conjetura ABC. Este problema de 40 años concierne a la ecuación a + b = c para enteros completos y las relaciones entre sus factores primos, con implicaciones para teoremas como el Último Teorema de Fermat. La prueba de Mochizuki se basa en su intrincada teoría de Teichmüller inter-universal (IUT), que muchos expertos encontraron difícil de penetrar.
El entusiasmo inicial disminuyó a medida que los esfuerzos de verificación se estancaron. En 2018, Peter Scholze de la Universidad de Bonn y Jakob Stix de la Universidad Goethe de Frankfurt identificaron un posible error, que Mochizuki disputó. Sin una autoridad central, el mundo matemático se dividió: la mayoría de los matemáticos en un lado, y un grupo más pequeño afiliado a Mochizuki y al Instituto de Investigación en Ciencias Matemáticas de Kioto en el otro.
Para romper el impasse, Mochizuki ahora aboga por formalizar la prueba en Lean, un lenguaje para matemáticas verificadas por computadora. Inspirado por una conferencia de julio en Tokio, argumenta en un informe reciente que Lean podría liberar la verdad matemática de las "dinámicas sociales y políticas". Como escribe, “[Lean] es la mejor y quizás la única tecnología… para lograr un progreso significativo con respecto al objetivo fundamental de liberar la verdad matemática del yugo de las dinámicas sociales y políticas.”
Los expertos ven promesa pero advierten precaución. Kevin Buzzard del Imperial College London nota: “Si está escrito en Lean, entonces no es una locura, ¿verdad? Mucho del contenido en los artículos está escrito en un lenguaje muy extraño, pero si puedes escribirlo en Lean, entonces significa que al menos este lenguaje extraño se ha convertido en algo completamente bien definido.” Johan Commelin de la Universidad de Utrecht agrega: “Queremos entender el porqué [de IUT], y hemos estado esperando eso por más de 10 años. Lean podría ayudarnos a entender esas respuestas.”
Sin embargo, la tarea es inmensa, requiriendo equipos de especialistas y potencialmente años de trabajo. Incluso el éxito podría no poner fin a los debates sobre interpretación, ya que Mochizuki reconoce que Lean no ofrece una "cura mágica" para los problemas sociales. Buzzard sigue optimista: “No puedes discutir con el software.”