Pierre de Fermat fue un matemático del siglo XVII.
Lebrecht Música y Artes, YAY Media AS/Alamy
En el vestíbulo de un hotel del centro de Londres, los turistas se preparan para un día de turismo en medio de una ola de calor. Mientras tanto, el personal está reacondicionando el comedor después del desayuno. Y en una sala de reuniones sin ventanas, los académicos reunidos contemplan si los humanos tienen un papel que desempeñar en el futuro de las matemáticas, ahora que la IA puede demostrar teoremas por sí sola.
El ambiente general en la sala es de desconcierto ante el reciente salto en la inteligencia informática y entusiasmo por el potencial que abre, y tal vez una ligera inquietud sobre lo que les depara el futuro personalmente.
Veinticinco investigadores de diversos campos y países están aquí para pasar una semana trabajando en la formalización del último teorema de Fermat con modelos de IA de vanguardia.
El último teorema de Fermat desconcertó a los matemáticos durante siglos hasta que fue demostrado en 1993 por Andrew Wiles. Afirma que no hay números enteros a, b y c que satisfagan la ecuación aⁿ + bⁿ = cⁿ, donde n es un número entero mayor que 2. Es extremadamente fácil de afirmar, pero diabólicamente difícil de probar.
Ahora, Kevin Buzzard del Imperial College de Londres está trabajando en un proyecto de cinco años para convertir las 100 páginas de matemáticas de Wiles en un código informático llamado Lean, de modo que pueda comprobarse formalmente su corrección y utilizarse como base para futuras investigaciones.
La formalización de teoremas matemáticos los saca del ámbito del lápiz y el papel y los coloca en una configuración que permite a las computadoras lidiar con ellos, trabajando metódicamente en la lógica y exponiendo cualquier falla. Ya hay 2 millones de líneas de matemáticas formalizadas almacenadas en un repositorio central llamado Mathlib.
Este taller ha reunido a matemáticos, informáticos y expertos en IA con la esperanza de que puedan avanzar en el proyecto de Buzzard de añadir el último teorema de Fermat a este corpus obteniendo los últimos modelos de IA para hacer parte del trabajo pesado.
Los grupos están agrupados alrededor de computadoras portátiles, cada una de las cuales muestra interfaces ligeramente diferentes para uno de los modelos líderes de la industria de la inteligencia artificial. El ambiente es bullicioso. Se reservó una segunda sala para que la gente pudiera trabajar en silencio si así lo preferían, pero está vacía.
Los problemas y subproblemas son divididos, distribuidos y eliminados por cerebros humanos que impulsan y dirigen la IA. Antes del taller había un total de 20.000 líneas de código en el proyecto, afirma Buzzard. Después del primer día, esa cifra se había duplicado.
El proyecto Formalizing Fermat se financió en 2024 y comenzó lentamente mientras Buzzard codificaba laboriosamente a mano. El ritmo se aceleró dramáticamente alrededor de diciembre del año pasado, dice, cuando el poder de los modelos de IA para trabajar con matemáticas avanzadas pareció crecer rápidamente. Luego, en mayo, una máquina resolvió un problema planteado por Paul Erdős hace 80 años, tomando al campo totalmente por sorpresa. Todo el asunto ha obligado a Buzzard a repensar las cosas.
“Siempre estuve tranquilamente confiado en que íbamos a tener éxito. Pero ahora, después de dos años, la IA se ha vuelto tan buena que mi instinto me dice que esto es ridículo; lo que dije que haría es ridículo. Hagamos algo 10 veces mejor”, dice.
La demostración de Wiles puede haberse extendido a unas 100 páginas, pero se basó en otras 2.000 páginas de matemáticas de los años 1960, 1970 y 1980. El proyecto original de Buzzard era formalizar sólo el artículo final (o al menos las mejoras más recientes del mismo), pero asumir que todo en lo que se basaba era correcto.
Si todo el conjunto de teoremas fuera una pirámide, Buzzard tenía la intención de empezar a ascender sólo desde el 90 por ciento del camino, donde residían los problemas realmente interesantes. Pero ahora cree que es posible abordar todo el asunto de arriba a abajo para que esté completo.
Tiene plena confianza en que, al final de su proyecto de cinco años, habrá hecho lo que se propuso originalmente. El progreso de la IA en los próximos años, lo caro que sea su acceso y cómo se desarrolle este taller determinarán hasta dónde llegará en el resto de la pirámide.
Hang Lu Su del Imperial College London es uno de los investigadores que participa en el taller. Usó ChatGPT para aprender Lean por sí misma hace solo seis meses y ahora está trabajando aquí a la vanguardia.
La mayoría de los matemáticos que conoce todavía usan lápiz y papel, por lo que el uso de la IA y la formalización que se muestran aquí no son de ninguna manera representativos del campo actual, pero ella cree que podría ser un vistazo a su futuro. “Siento que hay una industrialización del proceso intelectual. [occurring]”, dice Su. “En todo caso, las herramientas de IA están funcionando tan bien que es un poco como: ‘Está bien, simplemente dejamos [the AI model] Claude trabaja, ¿y luego qué hacemos?’”
Aquí se utiliza una variedad de herramientas, desde las gratuitas y de código abierto hasta los modelos más recientes y caros de empresas emergentes estadounidenses. Nadie en el evento puede decir con precisión cuánto dinero se gasta en tokens, las unidades de inteligencia artificial mediante las cuales se cobra el acceso, pero la mayoría está de acuerdo en que fácilmente ascenderá a miles de libras por día. “Estoy quemando fichas como si no estuviera pagando la factura, definitivamente”, dice Su.
Pero para resolver estos complicados problemas matemáticos, el grupo necesitará calidad además de cantidad. Su explica que ella y un colega estaban tratando de formalizar la misma parte de matemáticas el primer día del taller. Ella llegó a una solución de 800 palabras, mientras que su colega encontró una de 400 palabras. Se podría decir igualmente que ambos han demostrado el teorema en cuestión. Pero la versión más corta, compilada más rápido, sería más fácil para la IA en el futuro y también sería más fácil de comprender para un humano.
El código creado por la IA puede ser detallado, torpe y tardar mucho en ejecutarse, afirma Buzzard. A veces se basa en el uso de funciones oscuras dentro de Lean de manera no deseada, que no se compilarán correctamente cuando se publiquen versiones actualizadas.
Muchos de los curadores de la biblioteca Mathlib son cautelosos a la hora de añadir mucho código Lean generado por IA, incluso si demuestra teoremas, por esta misma razón, dice Buzzard. Actualmente, el código de esa biblioteca está escrito de manera experta y cuidadosa por matemáticos humanos, quienes garantizan que sea eficiente, conciso y legible para los humanos. Es una base sólida para el trabajo futuro. El código que se está creando en este taller es bastante diferente.
“Estamos construyendo una capa de sedimento en la parte superior, llamémosla simplemente sedimento, y ahora la pregunta es: ¿qué sucede cuando intentamos mover la siguiente capa? ¿Podemos construir la siguiente capa encima o simplemente se detiene?” pregunta Buzzard.
Estos avances también están planteando cuestiones filosóficas y existenciales para los matemáticos. Como mínimo, las herramientas disponibles para los investigadores están cambiando y, por lo tanto, también lo hará su trabajo, pero en el extremo más tecnooptimista del espectro, la IA puede terminar asumiendo y ampliando las fronteras de las matemáticas conocidas por sí sola, superando y reemplazando el pensamiento humano.
“Todos estamos haciendo [maths] porque nos encanta y creemos que es importante. Pero ahora está apareciendo la IA y, de repente, la pregunta es: ¿por qué hacemos esto? ¿Cuál es el punto de esto? dice Buzzard. “Si una máquina demuestra un teorema pero ningún humano puede entenderlo, ¿qué habremos logrado?”
Esas preguntas son aún más precisas cuando las matemáticas en cuestión son extremadamente abstractas y se ubican en el tipo de mundo que incluye esferas de 38 dimensiones o problemas complejos sin una aplicación inmediata obvia. “Existe este mundo abstracto, pero ¿existe ese mundo abstracto si los humanos no están ahí para apreciarlo?” pregunta Buzzard.
Temas: