El entrenamiento es la clave del éxito en la Olimpiada Internacional de Matemáticas (IMO). Las inteligencias artificiales prometen revolucionar dicho entrenamiento, como ya lo han hecho con el ajedrez; gracias a ellas hoy contamos con niños prodigio estratosféricos para su edad, como el argentino Faustino Oro, el maestro internacional más joven de la historia, con un ELO ~2400 y solo 10 años, o el turco Yagiz Erdogmus con un ELO ~2600 con 13 años. El primer gran paso lo ha dado una inteligencia artificial de Google DeepMind, como no podía ser de otro modo. La combinación de AlphaProof y AlphaGeometry 2 ha logrado resolver cuatro de los seis problemas de la IMO de 2024; hubiera logrado 28 puntos de los 42 (cada problema vale 7 puntos) y hubiera obtenido una medalla de plata (este año el umbral de oro fueron 29 puntos, que lograron 58 de los 609 competidores). Las soluciones fueron evaluadas por tres matemáticos: Timothy Gowers, medallista de oro de la OMI y Medalla Fields, y Joseph Myers, dos veces medallista de oro, y el presidente del Comité de selección de problemas de la OMI 2024. AlphaProof resolvió dos problemas de álgebra y un problema de teoría de números; entre ellos está el más difícil de este año, que solo 5 humanos lograron resolver. AlphaGeometry 2 logró resolver el problema de geometría. Pero los dos problemas de combinatoria superaron a la máquina. Un éxito increíble de estas inteligencias artificiales, que augura que en menos de un lustro todos los jóvenes participantes en la IMO se entrenarán usando IA.

Se trata de un primer éxito y queda mucha investigación pendiente hasta que las IA logren 42 puntos en la IMO en igualdad de condiciones que los humanos. En la IMO, los participantes disponen de 9 horas en dos días para resolver seis problemas (tres problemas en 4 horas y media cada día). Sin embargo, AlphaProof resolvió un problema en pocos minutos, pero para los otros necesitó hasta 60 horas (AlphaGometry 2 resolvió su problema en 19 segundos, siendo capaz de resolver el 83 % de todos los problemas de geometría de la historia de la OMI). Fuera de toda, muchos humanos habrían logrado superar a AlphaProof si hubieran dispuesto de 60 horas. Por otro lado, la IA no usó los enunciados originales, sino su traducción manual a Lean (el software de demostración automática de teoremas más usado); además, la solución de la IA estaba escrita en Lean (lo que permitía usar dicho software para validar la demostración). Siguiendo la línea de otras IA de DeepMind como AlphaZero, en la que está basada, AlphaProof aprendió sin ningún tipo ayuda, completamente sola, a resolver ~100 millones problemas de tipo IMO. Son muchos porque todos fueron formalizados en Lean gracias a una versión de Gemini, el LLM (gran modelo de lenguaje) de Google; Gemini formalizaba cada problema muchas veces, porque a veces cometía errores (alucinaciones) que conducían a problemas más sencillos que los originales. Se cree que esto pudo ayudar a AlphaProof a aprender mejor.

El fracaso con los problemas de combinatoria es debido a que este tipo de problemas son muy difíciles de formalizar. Por ejemplo, uno de los problemas requería encontrar la mejor estrategia para un juego determinado y hoy en día formalizar estrategias en Lean es muy complicado (aunque se están haciendo progresos que acabarán siendo usados por una futuro AlphaProof 2, o como acabe llamándose). Pero debemos ver más allá de este primer éxito. Las IA como AlphaProof acabarán afectando a la investigación en matemáticas. Por ahora es imposible predecir cómo lo harán, pero con seguridad se incorporarán como una herramienta más en manos del matemático profesional. Además, al ritmo exponencial que progresan las IA de DeepMind, cabe prever que el año próximo AlphaProof 2 será capaz de resolver los seis problemas de la IMO de 2025. Los avances en inteligencias artificiales y en demostradores automáticos de teoremas revolucionarán el entrenamiento de los jóvenes que quieran competir en las olimpiadas matemáticas. Tiempo al tiempo. Por cierto, DeepMind no ha publicado un artículo científico sobre este logro. Solo de dispone de información promocional en AlphaProof and AlphaGeometry teams, «AI achieves silver-medal standard solving International Mathematical Olympiad problems,» Google DeepMind, 25 Jul 2024, y de información divulgativa en este hilo de Timothy Gowers, @wtgowers, y en Davide Castelvecchi, «DeepMind hits milestone in solving maths problems — AI’s next grand challenge,» News, Nature, 25 Jul 2024.