Entre el 14 y el 16 de septiembre, el ICMAT acogió el workshop 'AI in Mathematics days', un encuentro que congregó a más de 100 investigadores e investigadoras, tanto de forma presencial como telemática. El evento se centró en el uso de herramientas de inteligencia artificial (IA) en la investigación matemática y en la formalización de demostraciones.
La noticia del posible avance de OpenAI en la resolución de las ecuaciones de Navier-Stokes, uno de los Problemas del Milenio, ha marcado un hito reciente en el campo. Investigadores como Diego Córdoba (CSIC en el ICMAT) y Luis Martínez-Zoroa (CUNEF Universidad) han señalado que este suceso marca el inicio de una nueva etapa en la investigación matemática.
El programa del workshop incluyó tres minicursos impartidos por expertos internacionales: María Inés de Frutos Fernández (Universität Bonn), Damien Galant (Brown University) y Mitchell Taylor (Oxford University). Taylor ofreció una visión general de las herramientas de IA aplicadas al trabajo matemático. Los vídeos de estos cursos estarán disponibles próximamente en el canal de YouTube del ICMAT.
Alberto Enciso y Ángel Castro, ambos del CSIC en el ICMAT y organizadores del evento, comentaron que el uso de la IA está ampliando el alcance del trabajo matemático y de otros campos, modificando tanto los métodos como los objetivos de la investigación.
Un tema central del encuentro fue la formalización de demostraciones matemáticas mediante programas como Lean. Esta herramienta permite verificar automáticamente la corrección de las demostraciones, ofreciendo una "garantía sobrehumana", según explicó De Frutos Fernández, especialista en el área. La IA, aunque capaz de generar nuevas demostraciones, requiere de esta formalización para asegurar su validez.
Las herramientas de formalización, como Lean, también facilitan una comprensión más profunda de la teoría subyacente y promueven el desarrollo de librerías de matemáticas formalizadas reutilizables. Otros asistentes de demostración mencionados incluyen Rocq, Isabelle, Mizar y Metamath, cada uno con aplicaciones específicas según el área de investigación.
