La Universidad Imperial de Londres está a la vanguardia de la investigación en matemáticas modernas, gracias al apoyo de Renaissance Philanthropy. Esta organización ha realizado una generosa donación que da inicio a un innovador proyecto de investigación de dos años, liderado por el Profesor Kevin Buzzard, del Departamento de Matemáticas. Este aporte marca el primer regalo recibido por parte de Renaissance Philanthropy y se enmarca dentro del AI for Math Fund, gestionado en colaboración con el donante fundador XTX Markets, destinado a impulsar proyectos que maximicen el uso de la inteligencia artificial.
El objetivo principal del proyecto es acelerar la investigación matemática contemporánea mediante la creación de un amplio conjunto de datos públicos que contenga declaraciones formalizadas extraídas de publicaciones recientes en revistas académicas. La traducción de conceptos matemáticos a un lenguaje formal con una sintaxis rigurosa no solo elimina ambigüedades para los humanos, sino que también permite que las computadoras interactúen con las matemáticas de maneras novedosas.
Avances significativos en la investigación matemática
A pesar de que herramientas digitales como asistentes de prueba e inteligencia artificial han mostrado potencial para generar pruebas matemáticas básicas de manera autónoma, las tecnologías actuales están limitadas a matemáticas a nivel escolar, distantes del ámbito investigativo que abordan los científicos hoy en día. El equipo del Profesor Buzzard se propone superar estas limitaciones al formalizar las declaraciones de cientos de teoremas complejos a nivel investigativo en diversas áreas matemáticas. Esto no solo ampliará el vocabulario disponible para los probadores modernos de teoremas, sino que también proporcionará un extenso y desafiante conjunto de datos para la autoformalización de sistemas de IA.
Con esta financiación, el Profesor Buzzard planea reclutar a cuatro investigadores posdoctorales para llevar a cabo investigaciones y ayudar en la construcción del conjunto de datos. Estos investigadores utilizarán Lean, un lenguaje de programación considerado como la mejor herramienta para la formalización matemática. El Departamento de Matemáticas de Imperial cuenta con numerosos expertos en Lean, lo que lo convierte en el entorno ideal para que estos investigadores crezcan y se desarrollen durante los próximos dos años.
El impacto transformador del apoyo filantrópico
Acelerar la formalización de las matemáticas es una parte necesaria para acelerar las propias matemáticas. Profesor Kevin Buzzard
El Profesor Buzzard enfatiza: “Para agilizar este proceso, necesitamos herramientas que puedan realizar el trabajo complejo de formalización o herramientas que apoyen a los humanos en esta tarea. Hemos visto cómo la IA apoya descubrimientos revolucionarios en campos como la medicina y la ingeniería, y creo que tiene un potencial inexplorado para las matemáticas”. Además, añade: “El apoyo filantrópico por parte de Renaissance Philanthropy nos está permitiendo cambiar el panorama actual de las matemáticas modernas, ayudando a los matemáticos a resolver desafíos presentes y futuros”.
A lo largo del tiempo, los investigadores han anhelado construir sistemas capaces de resolver problemas matemáticos profundos y abiertos por sí mismos. Sin embargo, actualmente, los sistemas de IA operando a este nivel suelen emplear lenguaje humano, lo que puede dar lugar a *alucinaciones*, donde la IA genera respuestas engañosas o incorrectas. El conjunto de datos creado por el equipo será crucial para cerrar esta brecha, proporcionando los datos necesarios para entrenar sistemas de IA con el fin de comprender mejor y eventualmente asistir en la formalización de declaraciones matemáticas más complejas.
Un futuro prometedor para las matemáticas y la IA
Demostrar cómo la IA puede acelerar el progreso en la investigación matemática incentivará a más matemáticos a adoptar estas tecnologías en su trabajo. Esto contribuirá al desarrollo y atracción del talento necesario en este campo esencial para avanzar en la formalización matemática.
Tom Kalil, CEO de Renaissance Philanthropy, expresó su entusiasmo por esta colaboración: “Estamos emocionados por la convergencia entre IA y matemáticas; donde la colaboración entre matemáticos e informáticos podría llevar al descubrimiento de nuevos teoremas matemáticos y mejorar las capacidades razonativas modelos AI”. Kalil también destacó su expectativa sobre cómo el proyecto del Profesor Buzzard transformará el campo.
El AI for Math Fund busca acelerar tanto el ritmo como el impacto del descubrimiento matemático apoyando proyectos con potencial para avanzar significativamente en este ámbito. Con un total disponible superior a 18 millones dólares en subvenciones, este fondo representa una inversión filantrópica significativa destinada al desarrollo herramientas basadas en inteligencia artificial y aprendizaje automático aplicadas a las matemáticas.
Si (
No(
