Un prototipo de Claude logró traducir la titánica demostración del último teorema de Fermat a trece millones de líneas de código informático verificadas a prueba de fallos. El logro pulverizó una tarea humana calculada en diez años y desató un terremoto sobre cómo validaremos la verdad científica de acá en adelante.
En 1637, el jurista y matemático francés Pierre de Fermat garabateó una nota al margen de un ejemplar de la Aritmética de Diofanto que torturaría a las mentes más brillantes del planeta durante más de tres siglos y medio. Con una picardía casi infantil, escribió que la ecuación xn + yn = zn no tiene soluciones con números enteros positivos cuando la potencia n es mayor que 2. Y remató con una frase legendaria: «Tengo una demostración verdaderamente maravillosa para este hecho, pero este margen es demasiado estrecho para contenerla».
Fermat murió sin dejar esa prueba escrita. Hizo falta que pasaran 357 años, incontables carreras frustradas y que el matemático británico Andrew Wiles se encerrara durante siete años en el altillo de su casa para que, en 1994 y con la colaboración de Richard Taylor, la humanidad pudiera cantar victoria. Aquel manuscrito monumental de cientos de páginas unió ramas de la matemática que parecían incompatibles y le valió a Wiles el prestigioso Premio Abel.
Pero en la ciencia contemporánea, entender un razonamiento no es lo mismo que tener la certeza matemática absoluta de que no se escapó ningún error microscópico en el camino. Por eso, lo que acaba de suceder en los laboratorios de la tecnológica Anthropic, en California, dejó a la comunidad científica con la mandíbula en el piso: un prototipo avanzado de su modelo Claude tradujo y certificó por computadora toda la prueba de Fermat en apenas 11 días continuos de cómputo. A los mejores matemáticos de carne y hueso del mundo les iba a tomar una década entera terminar ese mismo trabajo.
«El hecho de que una máquina haya podido convertir el laburo de matemáticos humanos en una demostración blindada de 13 millones de líneas de código simplemente me voló la cabeza», confesó Alex Kontorovich, teórico de números de la Universidad de Rutgers en Nueva Jersey, todavía asombrado por el anuncio.
La obsesión por no dejar ni un ladrillo suelto
Para comprender la magnitud de este hito hay que adentrarse en un concepto que viene revolucionando los claustros universitarios: la formalización matemática.
Hasta hoy, las demostraciones se publican en artículos científicos escritos en lenguaje humano. Tienen palabras, metáforas, saltos lógicos que se dan por sobreentendidos entre colegas y fórmulas en papel. Pero los humanos nos cansamos, nos distraemos y dejamos pasar baches lógicos. La formalización consiste en agarrar cada una de esas frases y traducirlas a un lenguaje de programación hiperestricto —en este caso, un software de código abierto llamado Lean—.
Fijate en la analogía: leer un paper tradicional es como recorrer un rascacielos a simple vista y asumir que la estructura es sólida porque no se tambalea; formalizarlo en Lean equivale a revisar con un nivel láser y un microscopio cada tornillo, cada viga y cada molécula de hormigón para verificar que no haya ni una sola fisura oculta. Si el compilador da luz verde, la demostración es computacionalmente perfecta.
Desde 2024, el matemático Kevin Buzzard, del Imperial College de Londres, venía liderando un esfuerzo internacional para formalizar la prueba de Fermat dentro de Mathlib, la gran biblioteca comunitaria donde los científicos cargan el conocimiento matemático mundial. Sus cálculos eran prudentes pero realistas: necesitarían cerca de diez años para escribir pacientemente los miles de teoremas intermedios necesarios. La inteligencia artificial se tragó esa década en menos de dos semanas.
«Antes de esto, yo estaba seguro en un 99,9% de que la demostración de Wiles era correcta. Ahora estoy seguro al 100%», sentenció Buzzard.
El banquete de las máquinas y el fantasma del código alienígena
El salto cualitativo es descomunal. En febrero pasado, los sistemas automatizados habían logrado certificar el trabajo de Maryna Viazovska sobre el empaquetamiento de esferas en dimensiones hiperbólicas, pero atacar el último teorema de Fermat jugaba en otra categoría. Como graficó Daniel Litt, especialista de la Universidad de Toronto: «Si pudieron formalizar el teorema de Fermat, probablemente puedan formalizar cualquier cosa en la matemática moderna».
Sin embargo, el festejo encierra una trampa que preocupa a los investigadores. Para lograr su hazaña en tiempo récord, Claude no consultó paso a paso a los humanos: generó sobre la marcha más de 29.500 teoremas intermedios para apuntalar su razonamiento.
El problema es que ese código no se parece al trabajo prolijo y artesanal de los matemáticos. Es un tejido masivo de trece millones de líneas que resuelve el problema de punta a punta, pero que no está diseñado para que otro científico pueda agarrar una de sus partes y reutilizarla en una investigación distinta.
Para Buzzard, este salto plantea un escenario paradójico: el riesgo de que florezcan múltiples bibliotecas de conocimiento generadas por inteligencias artificiales incompatibles entre sí, tan veloces e inmensas que los humanos no tengamos el tiempo material de curarlas ni integrarlas a las plataformas públicas. Una suerte de sabiduría blindada pero empaquetada en cajas negras.
El fin de la fe ciega en las revistas científicas
Más allá de Fermat, el impacto más urgente de esta tecnología golpea de lleno al sistema de evaluación científica. El circuito tradicional de arbitraje por pares (el famoso peer review) atraviesa una crisis global silenciosa: los papers se volvieron tan largos, abstractos y sofisticados que casi nadie tiene el tiempo o la energía de revisarlos renglón por renglón antes de darles el visto bueno en una revista prestigiosa.
«Hoy es un secreto a voces que la mayoría de los artículos publicados contienen errores, y algunos de ellos muy graves que escapan a la revisión de los colegas», advierte Frederick Manners, matemático de la Universidad de California en San Diego. Hay demostraciones teóricas de cientos de páginas que pasan décadas en un limbo académico: algunos afirman que están bien, otros sospechan que están mal y nadie se atreve a sentenciar el veredicto final.
Tener una herramienta capaz de tomar un borrador académico recién salido del horno, cotejarlo en minutos contra las leyes matemáticas fundamentales y certificar si el razonamiento se sostiene o señalar exactamente dónde falló el autor cambiaría las reglas del juego para siempre. La proeza sobre el viejo enigma de Fermat no es el final de un capítulo del siglo XVII; es el amanecer de una era donde las máquinas ya no solo resuelven cuentas, sino que auditan con frialdad implacable los límites de la mente humana.
CientíficaMente 