En el artículo «Mathesis: Towards formal theorem proving from natural languages», se aborda la limitación clave de los demostradores de teoremas: su dependencia de enunciados ya formalizados. El trabajo se centra en el paso crítico de la 'autoformalización' —la traducción a un lenguaje formal como Lean 4— y presenta Mathesis, un sistema integral diseñado para automatizar todo el proceso.

El sistema introduce un Mathesis-Autoformalizer entrenado mediante aprendizaje por refuerzo para optimizar la traducción a código Lean. Su rendimiento se evalúa con LeanScorer, y se pone a prueba en Gaokao-Formal, un nuevo y exigente banco de pruebas. Finalmente, Mathesis-Prover genera la demostración completa en Lean, asegurando que la prueba final sea verificable.

Los resultados demuestran que Mathesis alcanza un rendimiento de vanguardia en varios bancos de prueba. El análisis revela una conclusión crucial: las mejoras en la autoformalización impactan el éxito final mucho más que las mejoras en el demostrador. Esto se explica porque si el problema se traduce incorrectamente a código Lean, el demostrador recibe una tarea mal planteada y no puede generar una prueba válida, sin importar su potencia. El trabajo confirma así que una traducción inicial de alta calidad es el factor más determinante para el éxito del proceso.