El viernes 22 de mayo a las 17hs (hora Argentina) tendrá lugar la segunda sesión del "Coloquio del Núcleo de Matemáticas Aplicadas del AUGM 2026". Será en modalidad híbrida.

Expositor:
Mauricio Ayala-Rincón
(Universidade de Brasília / Universidade Federal de Goiás)

Título:
Collaborative Human-Interactive Theorem Proving (ITP) Meets Generative AI

• Resumen:

This talk will present a personal position on the inclusion of generative AI within the well-established and fruitful Human-ITP collaboration, consolidated by the famous de Bruijn's 'Automath Project' in the 1960's - 1970's. I will contextualize this position within our efforts to formalize algebraic theorems in the Prototype Verification System (PVS) and, more recently, to make preliminary advances towards responsibly adding the power of Large Language Models to the PVS mechanization process.

Joint work with Thaynara Arielly de Lima (UFG), Andréia Borges Avelar (UnB), Nikson Bernardes Fernandes Ferreira (UnB), André Luiz Galdino (UFCat), Bruno Berto de Oliveira Ribeiro(UnB), Mariano Miguel Moscato (AMA/NASA LaRC FM).