El artículo «Munkres' general topology autoformalized in Isabelle/HOL» presenta un experimento de autoformalización asistida por LLMs que tradujo el libro de topología de Munkres a código verificable en Isabelle/HOL, cubriendo desde espacios topológicos hasta teoría de la dimensión en 85.472 líneas de código.

La metodología consiste en escribir primero esqueletos de prueba con marcadores (sorry) y delegar los pasos de demostración al sistema automatizado Sledgehammer. Dos LLMs trabajaron en secuencia: ChatGPT 5.2 generó las definiciones y enunciados; Claude Opus 4.6 eliminó los huecos restantes hasta completar todas las pruebas.

El análisis cualitativo revela que los teoremas son correctos aunque el código es imperfecto: algunas definiciones son más débiles de lo necesario, ciertos enunciados omiten cláusulas del libro original y las pruebas carecen de un paso de optimización. Los autores estiman que una revisión experta de pocos días bastaría para elevar la calidad de la librería.