El profesor Brent Yorgey publica una demostración completa, desarrollada desde cero, del Teorema Fundamental de la Aritmética en el asistente de pruebas Agda. El recurso está pensado como material didáctico de nivel intermedio para personas que ya conocen los fundamentos de Agda y la correspondencia de Curry-Howard, y que quieran estudiar un ejemplo extenso de prueba formalizada.
El trabajo surgió a partir de la búsqueda de proyectos finales para su curso de Programación Funcional. Tras probar durante una hora la formalización, Yorgey concluyó que resultaba demasiado compleja para sus estudiantes, pero continuó hasta completarla en aproximadamente una semana, sin recurrir a la biblioteca estándar de Agda ni a material de referencia. La versión actual únicamente demuestra la parte de existencia: dado un número natural, Agda devuelve su factorización en primos, lo que equivale a un programa de factorización verificado formalmente.
El artículo se estructura en bloques progresivos: lógica básica, igualdad, números naturales, suma, multiplicación, desigualdad, divisibilidad, primalidad, listas y, finalmente, el teorema completo. Cada sección cuenta con una explicación detallada del razonamiento y de las técnicas empleadas.
Se ofrecen dos versiones del documento: una completa, disponible como archivo literate Agda en el repositorio de GitHub del autor, y otra con huecos para que quien estudie pueda intentar rellenar las demostraciones por su cuenta. Yorgey sugiere descargar esta última y completar las pruebas antes de consultar la solución.