Ayer se publicó un artículo que muestra el uso de la formalización con Isabelle en el desarrollo de la investigación matemática. Su título es Diophantine equations over Z: Universal bounds and parallel formalization y en sus conclusiones dice:

Nuestro proyecto demuestra que formalizar matemáticas altamente técnicas puede brindar beneficios reales, corrigiendo muchos errores mientras mejora la claridad y fiabilidad. El tiempo y esfuerzo adicional requeridos no pueden ignorarse, pero quedan compensados por las ventajas aquí expuestas.

En retrospectiva, identificamos dos factores clave que contribuyeron al éxito de este proyecto. En primer lugar, fue crucial apoyarnos en nuestra experiencia previa formalizando el ya consolidado teorema DPRM para tomar decisiones importantes en este proyecto. A quienes estén interesados en formalizar sus matemáticas, les recomendamos comenzar con un proyecto más pequeño cuyo objetivo sea formalizar un teorema ya establecido. En segundo lugar, fue de gran ayuda contar con un equipo interdisciplinario de personas con distintas habilidades. En nuestro caso, esto incluyó tanto a matemáticos puros como a informáticos, y fue su esfuerzo conjunto lo que permitió tender un puente desde las pruebas en lenguaje natural hasta el metalenguaje en el que está programado el propio Isabelle.

Fomentar que los matemáticos integren asistentes de prueba en su flujo de trabajo ahora ayudará a moldear el desarrollo de herramientas mejores, haciendo que la formalización en sistemas como Isabelle o Lean llegue a ser tan fluida como escribir en LaTeX. Esto se ve reforzado por los recientes avances en IA, que sugieren que pronto podrían surgir potentes herramientas de automatización para la formalización. Al formalizar las matemáticas ahora, aseguramos que nuestros campos se beneficien de la IA y la automatización a medida que estas herramientas evolucionen.