Cuando la IA resuelve en días lo que toma años, ¿para qué hacer matemáticas?

A principios de este año, Sidharth Hariharan, un estudiante de posgrado de matemáticas de la Universidad Carnegie Mellon, recibió una noticia que le hizo correr a la oficina de su tutor con lágrimas en los ojos.

Acababa de recibir un correo electrónico de Maryna Viazovska, profesora de la École Polytechnique Fédérale de Lausanne en Suiza y ganadora en 2022 de la Medalla Fields, el mayor honor en matemáticas.

Durante más de dos años, ella y Hariharan habían estado al frente de un equipo de seis matemáticos en un esfuerzo por desglosar una de las demostraciones más célebres de Viazovska en pasos lógicos distintos, una tarea conocida como formalización.

Pero unas horas antes, Viazovska había recibido un aviso de un colega: les habían ganado.

O, como ella pronto comenzó a decir con cierta ironía, les habían "gaussado".

Gauss es un sistema de inteligencia artificial creado por Math, Inc., una empresa emergente de California. El sistema había tomado la hoja de ruta del equipo para formalizar el resultado de Viazovska --una solución a la disposición más densa posible de esferas en ocho dimensiones, conocida popularmente como el problema del empaquetamiento de esferas-- y la había completado en apenas cinco días.

Aunque la IA se asocia popularmente con tropiezos en aritmética (como el ya mítico error de ChatGPT al no contar correctamente el número de erres en la palabra "strawberry"), las empresas tecnológicas han invertido enormes recursos en sistemas de razonamiento capaces de resolver problemas matemáticos abiertos. Los avances recientes se han convertido en una carrera armamentística entre competidores de IA ansiosos por demostrar la inteligencia artificial a través del éxito en un campo que a menudo se presenta como la cúspide del intelecto humano.

A finales de mayo, OpenAI anunció que uno de sus modelos había refutado un teorema de 80 años de antigüedad que los matemáticos habían dado por cierto durante mucho tiempo; Google DeepMind siguió sus pasos con soluciones a otros nueve. Luego, solo unos días después de que OpenAI publicara su resultado, un equipo de matemáticos utilizó las mismas técnicas para resolver otro teorema abierto, lo que apunta al potencial de la IA para convertirse en una herramienta útil, o incluso en un socio, para los matemáticos que exploran nuevas ideas.

"Hace unos 12 meses, aún se podía decir que se trataba de curiosidades o exageraciones y que no podían ser útiles", dijo Terence Tao, matemático ganador de la Medalla Fields de la Universidad de California en Los Ángeles. "Ahora ya no se puede sostener esa postura".

Para los miles de estudiantes de posgrado en Estados Unidos que actualmente imaginan su futuro en las matemáticas puras, y quienes aprenden el oficio a través de muchas de las mismas habilidades y problemas que la IA está empezando a dominar, puede ser difícil evitar los pronósticos sombríos.

El artículo de OpenAI fue un "shock", dijo Carl Schildkraut, un estudiante de posgrado de la Universidad de Stanford que trabajó en el artículo de seguimiento que amplió la técnica de la IA, y añadió que sus compañeros de posgrado "en general, no eran optimistas" sobre sus perspectivas. Pero un análisis más detenido del resultado también le hizo apreciar las limitaciones de las matemáticas generadas por inteligencia artificial.

"Cuando los humanos trabajamos en matemáticas, a menudo nos hacemos preguntas como: "¿Qué ideas estoy construyendo?" o "¿Qué está pasando aquí realmente?", dijo.

A principios de junio, un grupo internacional de matemáticos publicó una declaración en la que se reconocían los beneficios de la IA, pero también instaba a la cautela. A los matemáticos les preocupa la falta de voluntad de las empresas de IA para revelar información básica sobre sus métodos, su incapacidad para reconocer adecuadamente a los autores humanos y su afán por equiparar la destreza matemática con la idea de la superinteligencia de las máquinas. El eslogan de Math, Inc., por ejemplo, es: "Resuelve las matemáticas, resuelve todo".

Patrick Massot, matemático del Laboratoire de Mathématiques d'Orsay en Francia, comparó la primicia de la empresa con una "bomba atómica" que haría que los proyectos fueran radioactivos para los jóvenes matemáticos, incluso si eso significaba perder una formación valiosa o la oportunidad de desarrollar nuevas ideas.

La primicia también puso de manifiesto algunos de los temores latentes sobre lo que se pierde con la automatización. Algunos matemáticos no solo lo han visto como una violación de la etiqueta académica, sino como una amenaza para el futuro del campo: si cualquiera puede ser "gausseado", ¿por qué se van a molestar los académicos en resolver ciertos problemas?

¿Y por qué alguien habría de pagarles por eso?

'Te preguntas si todo fue en vano'

El problema del empaquetamiento de esferas es fácil de visualizar en tres dimensiones: imagina una pila de naranjas en un puesto del mercado. ¿Cuál es la configuración más compacta posible? La respuesta, propuesta por primera vez hace 400 años, es exactamente la pila de fruta que te imaginaste, pero es difícil descartar todas las demás posibilidades. Los matemáticos no lograron demostrarlo hasta 1998.

El empaquetamiento de esferas en dimensiones superiores, como la octava, es más difícil de visualizar porque implica puntos en el espacio definidos por más de tres números. La demostración de Viazovska forjó conexiones sorprendentes entre dos subcampos diferentes de las matemáticas, la geometría y la teoría de números, conexiones que el equipo esperaba explorar con más detalle al formalizar la prueba.

Cuando Hariharan se acercó a ella para hablar de formalizar su solución, ella lo vio como una oportunidad de aprendizaje. "Quizá la forma más fácil sería formalizar algo más sencillo por mi cuenta", dijo Viazovska. "Pero eso no es muy divertido".

Al principio, ella le enseñó los conceptos de alto nivel mientras él le enseñaba el software, llamado Lean, que utilizarían en su trabajo. Luego, junto con otros cuatro matemáticos, desarrollaron una hoja de ruta para detallar la lógica de su demostración, paso a paso.

Tras aproximadamente un año de trabajo, el grupo abrió el proyecto a colaboradores externos. No fue ninguna sorpresa que varias empresas de IA, que usan Lean para enseñarles matemáticas a sus sistemas, se sumaran para ayudar. Pero en aquel momento, los mejores sistemas solo podían generar pequeños fragmentos de código útil.

Así que el otoño pasado, cuando Math, Inc. le dijo al grupo que Gauss había resuelto unas 30 partes sin terminar de la demostración, Hariharan y sus colegas se mostraron entusiasmados. Le pidieron a la empresa que compartiera todos los resultados. En cambio, la compañía dejó de dar señales de vida.

Auguste Poiroux, estudiante de doctorado en la École Polytechnique quien también trabaja para Math, Inc., dijo que la empresa había centrado su atención en una nueva versión de Gauss. La compañía decidió volver al problema del empaquetamiento de esferas solo unos meses después, utilizándolo como caso de prueba para su sistema mejorado.

Para sorpresa de todos, dijo Poiroux, el Gauss mejorado completó toda la demostración.

Viazovska quedó aún más sorprendida cuando un emocionado Poiroux le mostró un adelanto de la solución "accidental", como él la describió. "Enseguida me di cuenta de que ella no compartía mi entusiasmo", dijo. Le pidió que esperara antes de informar a Hariharan, a quien ella le envió un correo electrónico poco después.

De inmediato, Hariharan llamó a sus padres en Dubái. "Te preguntas si todo fue en vano", dijo. "¿Por qué te pasaste dos años de tu vida en esto, para empezar?".

"Confía en tu gurú", le dijeron sus padres. "Confía en el proceso".

Esa noche, Jesse Han, director ejecutivo de Math, Inc., le envió un mensaje a Hariharan diciéndole que estaba abordando un vuelo nocturno a Pittsburgh. Se reunieron en un Starbucks a la mañana siguiente, junto con el asesor de Hariharan, Jeremy Avigad, quien salió corriendo del gimnasio tras "la ducha más rápida de su vida", según recuerda. Después de que Han propusiera divulgar el resultado de inmediato y pasar a un proyecto de formalización relacionado, los académicos estallaron, argumentando que el objetivo original del proyecto, comprender mejor la demostración de Viazovska, estaba lejos de haberse cumplido.

"El resultado en sí es, sin duda, muy impresionante, pero tampoco es lo que queríamos para nuestro proyecto", dijo Hariharan.

Pero tras hablar con otros matemáticos y revisar el código, finalmente acordaron una declaración en la que se reconocía que Gauss había elaborado una formalización correcta meses antes de lo previsto.

También concluyeron que aún quedaban meses de trabajo por delante para que ese código fuera realmente útil para la gente. "Aún queríamos hacerlo", dijo Hariharan.

La prisa por 'declarar la victoria'

Una forma de entender la situación a la que se enfrentan los jóvenes matemáticos es como una versión acelerada de la automatización que afecta al trabajo en otras industrias, lo que conlleva tanto oportunidades como temores de obsolescencia.

"Sabía por experiencia propia lo que era ser estudiante de doctorado y tener toda tu identidad ligada a un proyecto como este", dijo Han, quien formalizó un resultado importante durante su doctorado. Pero por mucho que aprendiera durante ese proceso, creía que habría llegado mucho más lejos con la ayuda de la IA. "Me habría encantado que se hubiera obtenido este tipo de resultado", dijo.

Han dijo que la primicia no fue intencionada --una consecuencia de las mejoras vertiginosas de la IA-- y que había esperado una respuesta "celebratoria". En cambio, se sintió "emboscado" por los mensajes furiosos de excompañeros, dijo, que comenzaron cuando aterrizó aquella mañana de invierno en Pittsburgh y no habían cesado desde entonces.

Talia Ringer, una informática que estudia formalización en la Universidad de Illinois, dijo que la consternación que se extendió por los departamentos de matemáticas era similar a lo que ellos sintieron recientemente como estudiantes de posgrado en informática cuando la automatización llegó a la programación.

"No iban a apropiarse del trabajo que yo estaba haciendo, pero sí iban a afirmar que se apropiarían del trabajo que yo estaba haciendo", dijo Ringer.

Según Vaughan McDonald, estudiante de doctorado en matemáticas de quinto año en Stanford, el afán de las empresas de IA por "declararse vencedoras" ante ciertos problemas implica que, incluso cuando se reconoce el trabajo humano que hizo posible la automatización, generalmente no aparece en los titulares. Esto ha contribuido a generar cierta satisfacción ante el fracaso ajeno en un campo académico tan prestigioso.

"La gente dice: 'Oh, no debería haber trabajos de matemáticas. Resígnense, matemáticos'", dijo McDonald. "Me parece terrible".

Los matemáticos señalan un desequilibrio de poder entre los departamentos de matemáticas, cada vez más reducidos, y las empresas bien financiadas, que pueden optar por gastar sumas equivalentes al financiamiento anual de varios estudiantes de posgrado en un solo problema. Un empleado de Math, Inc. le dijo al equipo de Hariharan que la empresa había gastado más de 100.000 dólares en calcular la solución del empaquetamiento de esferas.

Pero los matemáticos aportan un "valor tremendo" a la IA, dijo McDonald, gracias al trabajo intelectual que realizan para posibilitar la automatización. "No se les reconoce ni se les compensa adecuadamente por ello", afirmó.

En ocasiones, las tensiones han desembocado en rencor público. Cuando Han habló en una reunión de Exponentiating Mathematics, un programa del Departamento de Defensa, volvió a describir el proyecto de empaquetamiento de esferas como "terminado" e identificó erróneamente a los autores originales. Avigad se levantó entonces y "le dio su merecido", como él mismo dijo más tarde, ante una multitud de matemáticos atónitos. El comportamiento de la empresa "no fue bueno para ellos; no fue bueno para las matemáticas; no fue bueno para nadie", recordó haber dicho.

Tras finalizar la intervención de Avigad, un sonoro "¡guau!" rompió el silencio de la sala.

Han dijo que se trataba de malentendidos, pero que el "miedo y el ludismo" en respuesta había "endurecido mi determinación" de usar la IA para "formalizar todas las matemáticas".

Mientras tanto, el equipo de Hariharan está utilizando herramientas de IA para optimizar el código de Math, Inc. para la demostración del empaquetamiento de esferas, colaborando con Poiroux para eliminar las declaraciones redundantes (como teoremas que demuestran por qué 2+2 = 4) y convertir las secciones más crípticas en lenguaje legible. Aunque a veces es una tarea ardua, Hariharan dijo que el proceso había aportado "una cantidad no nula de conocimientos", tanto sobre las matemáticas de Viazovska como sobre cómo funciona la IA.

Hariharan también hace prácticas este verano en Axiom Math, otra empresa emergente de matemáticas con inteligencia artificial, aunque dijo que no está seguro del papel que jugará la inteligencia artificial en sus planes a largo plazo. Pero cuando regrese a sus estudios este otoño, su próximo proyecto no se centrará en la formalización.

"El próximo teorema que formalice, quiero haber sido yo quien lo haya demostrado", dijo.