El Comité de la Olimpiada Internacional de Matemáticas (IMO) ha lanzado lo que afirma ser la colección más grande del mundo de problemas de matemáticas a nivel de olimpiada, ahora disponible gratuitamente para todos. Según la información proporcionada, el archivo, llamado “IMO Vault”, incluye más de 45.000 problemas que abarcan álgebra, combinatoria, geometría y teoría de números, provenientes de olimpiadas nacionales desde 1959.
La colección no solo reúne los problemas, sino también sus soluciones verificadas por humanos, expresadas en lenguajes formales como Lean 4 e Isabelle/HOL, lo que la convierte en un recurso valioso para el entrenamiento de modelos de inteligencia artificial en razonamiento formal. Cada problema está etiquetado con metadatos que incluyen su nivel de dificultad (en una escala del 1 al 7, alineada con los criterios de evaluación de la IMO), los dominios matemáticos requeridos, la longitud de la solución en pasos y variantes conocidas.
El proyecto destaca por su enfoque en la legibilidad para máquinas: a diferencia de repositorios como AoPS o Art of Problem Solving, el IMO Vault está diseñado para ser directamente utilizable en sistemas de IA neuro-simbólica. Según pruebas internas compartidas por el equipo detrás de la iniciativa, ajustar un modelo de lenguaje de 7B parámetros con solo el 10% de este corpus mejoró su rendimiento en el benchmark MiniF2F del 41,3% al 58,7%.
Aunque el portal público es sencillo —construido con SvelteKit y alojado en Cloudflare Pages—, el verdadero potencial reside en su API abierta, que permite filtrar problemas por tema, año, país e incluso técnicas matemáticas específicas. Todo el material se distribuye bajo una licencia MIT y está alojado en GitHub.
