Una de las líneas de desarrollo de la Lógica Computacional es abordar formalizaciones de resultados matemáticos complejos. El intento de formalización produce como efectos laterales la formalización del conocimiento implícito en el resultado (el mathware) y el desarrollo de nuevos procedimientos de decisión.

Uno de los grandes retos actuales es la formalización de la demostración de Andrew Wiles del último teorema de Fermat. Una descripción detallada del reto se encuentra en el artículo Computer verification of Wiles’ proof of Fermat’s Last Theorem de Wim H. Hesselink. En el artículo se traza la hoja de ruta de la formalización describiendo la estructura de la demostración de Wiles. Una de las principales dificultades radica en comentando la necesidad de disponer de sistemas de razonamiento que incorporen cálculo simbólico. Hesselink estima que se tardarán unos 50 años en conseguirse la formalización del teorema de Wiles.