tl; dr No.
Incluso expresar las matemáticas convencionales y bien aceptadas en un verificador de pruebas es extremadamente difícil. Es un logro importante cuando logran verificar formalmente el tipo de cosas que aprendí en mi segundo año de universidad. La idea de formalizar toda una nueva área de las matemáticas y al mismo tiempo descubrirla es ridícula.
Además de eso, a nadie le importa si se sabe que la conjetura ABC es cierta o no; lo que nos importa es entender la razón por la cual es verdad, y tener una prueba verificada por computadora por sí sola no ayuda con eso. Existe un famoso problema conocido como el Problema de los cuatro colores que solo se ha resuelto mediante comprobaciones informáticas masivas, y es una gran decepción que no sepamos cómo hacerlo sin ellos: no tiene mucho sentido saber que algo es cierto si no sabes por qué es cierto de una manera que se ajusta dentro de tu cabeza.
- ¿Qué filósofos criticaron las matemáticas? ¿Por qué?
- ¿Cómo puede una persona hacer matemáticas rápidas?
- ¿Qué se entiende por "en la teoría de conjuntos podemos construir las estructuras de todo tipo"?
- ¿Cuál es la matemática de hacerse popular?
- ¿Cuál es el significado del teorema de representación de Riesz?
A la larga, si resulta que puedes usar la teoría de Mochizuki para resolver la conjetura ABC, eventualmente en una generación más o menos todos los nuevos matemáticos aprenderán aspectos de su teoría en la escuela. Por lo que puedo decir, esto significa (entre otras cosas) tomar la lógica matemática moderna de las afueras de las matemáticas y volver a colocarla en el centro, lo que será un cambio importante en la forma en que pensamos sobre las matemáticas, y que presumiblemente tendrá mucho más -alcanzar aplicaciones que solo la conjetura ABC sola.
