La IA demuestra teoremas. ¿Quién lo comprueba?

Divulgativa

Lean es un lenguaje de programación que nos permite escribir matemáticas que pueden ser verificadas por un ordenador, garantizando su corrección. En un momento en el que cada vez más áreas de la investigación cuentan con apenas un puñado de expertos y la IA avanza rápidamente como herramienta para el razonamiento matemático, esta garantía tiene mucho valor: cualquier error lógico, ya sea cometido por una persona o por un modelo de IA, queda en evidencia al trabajar con Lean. Lean ofrece un lenguaje cercano a la notación matemática habitual y herramientas que automatizan parte del trabajo mecánico de una demostración. A ello se suman librerías de resultados reutilizable como Mathlib, mantenida por la comunidad, o Tau Ceti, construida por IA bajo supervisión humana, que aspiran a alcanzar a la vanguardia de la investigación. Todo esto hace posible trabajar con Lean en matemáticas del más alto nivel como pueden ser el último teorema de Fermat o el reciente contraejemplo a la regularidad global de las ecuaciones de Navier–Stokes dado por OpenAI. Charla impartida por Pepa Montero Jimena y Enrique Díaz Blanco.

Horarios:

jueves 19 de noviembre a las 17:00

Duración:

1 hora

Lugar:

E.T.S. de Ingenieros Informáticos, H1003 (podría cambiar)

Direccion:

Organizador:

ANGEL HERRANZ NIEVA

Dirigida a:

Estudiantes, PDI

Cookie	Finalidad	Caducidad	Tipo de cookie	Responsable
ASP.NET_SessionId	Hacen posible el control de tráfico desde el servidor a múltiples usuarios a la vez, la identificación y el acceso como usuario.	Cierre de sesión / Fin de proyecto	Sesión	Inspiranetwork
cookiesDirective	Hacen posible recordar la configuración de las cookies.	Cierre de sesión / Fin de proyecto	Sesión	Inspiranetwork

La IA demuestra teoremas. ¿Quién lo comprueba?

Divulgativa

Horarios:

Duración:

Lugar:

Direccion:

Organizador:

Dirigida a:

Abierto:

Aforo:

Idioma:

Inscribirse como Participante

Selecciona el horario :