Este artículo presenta el "Mathematics Distillation Challenge – Teorías Ecuacionales", una iniciativa innovadora para avanzar en la investigación matemática a través de la colaboración y la asistencia de la inteligencia artificial. Tradicionalmente, la investigación matemática se ha centrado en un pequeño grupo de expertos, pero el proyecto busca ampliar esta colaboración a una comunidad más amplia de personas con conocimientos matemáticos.
El proyecto Teorías Ecuacionales (TEP) ya ha logrado resolver más de 22 millones de problemas de álgebra universal utilizando Lean (un sistema de formalización) y sistemas de demostración automática. El desafío actual se inspira en este trabajo y busca "destilar" este vasto conjunto de resultados en un conjunto conciso de reglas o un "cheat sheet" que pueda ser comprendido por humanos. La analogía es con un estudiante que resume el conocimiento de un curso en una hoja para usar en un examen.
El desafío consiste en crear un 'cheat sheet' de hasta 10 kilobytes que mejore el rendimiento de modelos de IA más pequeños (y económicos) en la resolución de problemas de álgebra universal. Estos modelos, por sí solos, tienen una precisión cercana al azar (50%), pero con la guía adecuada (el 'cheat sheet'), pueden alcanzar una precisión del 55-60%. Se proporciona una plataforma de pruebas para evaluar los 'cheat sheets' contra un conjunto de problemas, incluyendo algunos diseñados para ser más difíciles.
La primera etapa del desafío se centra en la creación de estos 'cheat sheets'. Los 1000 mejores participantes avanzarán a una segunda etapa, donde deberán no solo proporcionar la respuesta correcta (verdadero o falso), sino también una prueba o contraejemplo. El objetivo final es identificar las técnicas más efectivas para resolver estos problemas y potencialmente aplicar estos métodos a otras áreas de las matemáticas. El proyecto está siendo impulsado por la SAIR Foundation y busca fomentar una nueva forma de colaboración matemática, aprovechando el poder de la IA y la inteligencia colectiva. Se espera que este piloto abra la puerta a desafíos similares en otras áreas de las matemáticas, permitiendo una mejor comprensión de la resolubilidad de diferentes tipos de problemas matemáticos.
Un ejemplo de problema típico que el TEP puede resolver es: 'Si para todo x, x * x = x, ¿es cierto que para todo x, x = 0?' La resolución implica manipular la ecuación inicial o encontrar un contraejemplo.