Una demostración que nadie puede abarcar por sí solo

1. Un aplauso cortés

El 22 de julio de 1976, Kenneth Appel y Wolfgang Haken, dos matemáticos de la Universidad de Illinois, anunciaron que cuatro colores bastaban. Bajo las condiciones habituales de un mapa plano, se podía colorear cualquier mapa de modo que dos regiones con un tramo de frontera en común tuvieran distinto color; tocarse en un solo punto no contaba como ser vecinas. Aquel agosto, en la reunión anual de verano de la Sociedad Matemática Americana y la Asociación Matemática de América, celebrada en la Universidad de Toronto, Haken subió al estrado para explicar la demostración. Tenía cuarenta y ocho años, había nacido en Berlín y era topólogo, ya muy conocido por su trabajo sobre las formas del espacio tridimensional. La sala estaba abarrotada. Un problema pendiente desde hacía ciento veinticuatro años acababa de quedar resuelto.

Donald Albers estaba entre el público. Según contó después, esperaba que el final de la exposición de Haken desatara una ovación; lo que oyó fue un aplauso cortés. Al salir, un matemático tras otro expresó su inquietud. Les inquietaba la forma de aquella demostración. Una gran parte la había calculado una máquina: mil doscientas horas de cálculo que ninguna persona podía repasar de principio a fin a mano. Una y otra vez surgía la sospecha de que entre los cientos de páginas impresas se escondiera algún error. Albers añadió por su cuenta una pregunta: ¿no estarían deseando que lo hubiera? Su crónica apareció en una revista de matemáticas en la primavera de 1981. Su título empezaba con Un aplauso cortés y seguía con una pregunta: ¿qué es hoy una demostración?

El problema se entiende con una sola explicación, incluso de niño, y nació de algo igual de sencillo. En 1852, un joven llamado Francis Guthrie estaba coloreando un mapa de los condados de Inglaterra cuando observó que cuatro colores parecían bastar siempre. Se lo contó a su hermano Frederick, que se lo preguntó a su profesor, De Morgan. El 23 de octubre, De Morgan escribió a Hamilton, en Dublín, para hacerle llegar la pregunta. La carta comenzaba diciendo, en esencia, que un alumno le había pedido aquel día una razón para un hecho que antes no sabía que fuera un hecho, y que seguía sin saber si lo era. Hamilton contestó tres días después: no parecía probable que fuera a ocuparse pronto de aquel cuaternión de colores de su corresponsal. Los cuaterniones los había inventado él nueve años antes. El día del hallazgo había grabado la fórmula en la piedra de un puente por el que pasaba. Por aquellos años vivía enteramente metido en ellos.

El joven que había planteado la pregunta tenía entonces veintiún años y acababa de obtener su título de Derecho. Nunca volvió a ocuparse del problema ni escribió una sola palabra sobre él. Se marchó a Sudáfrica y pasó más de veinte años como profesor de matemáticas en el South African College de Ciudad del Cabo. El resto de su atención se lo llevaron los brezos del Cabo, que estudió junto a un botánico hasta su muerte. Un género de plantas lleva su apellido.

Hacía falta menos de un minuto para enunciar el problema y habían hecho falta ciento veinticuatro años para demostrarlo. Pero, para entender la inquietud de aquel día en Toronto, hay que volver atrás: el problema ya había sido demostrado una vez.

2. Una demostración que vivió once años

Durante más de veinte años, la pregunta durmió en un cajón. El 13 de junio de 1878, en una reunión de la Sociedad Matemática de Londres, Cayley preguntó si alguien la había resuelto. Al año siguiente apareció un antiguo alumno suyo. En julio de 1879, Alfred Kempe, un abogado londinense que ejercía ante los tribunales, anunció una demostración en Nature; el texto completo se publicó después en una revista matemática estadounidense. Su oficio eran los pleitos. Las matemáticas las había aprendido con Cayley en Cambridge. El argumento era claro y la idea, ingeniosa: si varias regiones forman una cadena en la que se alternan dos colores, se pueden intercambiar ambos a lo largo de toda la cadena sin tocar el resto del mapa. Es lo que después se llamaría una cadena de Kempe. La demostración se aceptó como válida. Y así permaneció once años. Un año después del anuncio de Kempe, el físico escocés Tait presentó otras dos demostraciones, con ideas brillantes y errores elementales. Por entonces, muchos daban el problema por cerrado.

En 1890, Heawood, profesor de matemáticas en Durham, señaló el fallo de Kempe. Al tratar una región rodeada por cinco vecinas, el argumento necesitaba efectuar dos intercambios de colores sucesivos. Kempe suponía que uno no interfería con el otro. Pero las dos cadenas podían enredarse en el mapa: el primer intercambio podía destruir las condiciones necesarias para efectuar el segundo. La demostración se vino abajo.

Heawood no se limitó a derribarla. Con las herramientas que quedaban entre los escombros obtuvo un resultado más débil: cinco colores bastan siempre. También sobrevivió la técnica de intercambiar los colores de una cadena entera, que pasó a formar parte del instrumental habitual de la teoría de grafos. Que una demostración fallida deje algo aprovechable no es raro en la historia de las matemáticas. Heawood, por su parte, llegó a catedrático en Durham, fue vicerrector entre 1926 y 1928 y siguió trabajando en la coloración de mapas durante casi sesenta años más. Su último artículo sobre el tema apareció en 1949, cuando tenía ochenta y siete u ochenta y ocho años. Sus colegas lo recordaban menudo, delgado, algo encorvado, con una barba enorme y una capa de corte extraño que a todas luces había conocido tiempos mejores. Un perro tenía permiso para quedarse en el aula durante sus clases.

Lo extraordinario era el tiempo transcurrido. Durante once años, una demostración escrita con toda claridad había estado ante los ojos de matemáticos de primera fila sin que nadie encontrara el error. Que una persona pueda leer una demostración nunca ha significado que alguien la haya comprobado de verdad. De ahí venía la mitad de la inquietud de Toronto: si eso pasaba con las demostraciones que una persona podía leer, ¿por qué confiar en una que no podía leer?

3. La sala de ordenadores de Illinois

Antes de Appel y Haken, el alemán Heinrich Heesch ya había puesto ordenadores a trabajar en esa dirección. En la década de 1960 había dado forma a un procedimiento decisivo. Haken acudió a él en 1967 por el problema de los cuatro colores. Durante los cuatro años siguientes, Heesch viajó varias veces a Estados Unidos: allí los ordenadores eran más grandes y más rápidos. Haken figuraba entre sus colaboradores. En el momento más importante, la Fundación Alemana de Investigación le retiró la financiación.

A comienzos de los años setenta, Haken contó en una conferencia los intentos que habían hecho con el ordenador del Laboratorio de Brookhaven. Según los expertos en informática a los que había consultado, por la vía del cálculo no había nada que hacer. Al terminar, Appel, un compañero de departamento, fue a hablar con él. Los expertos se equivocaban, le dijo: llevaría tiempo, pero era posible. Empezaron a colaborar en 1972. Appel se ocupaba sobre todo de los cálculos; Haken, de la parte teórica.

No escribieron primero una demostración convencional para dejarle al ordenador unas cuantas cuentas al final. La máquina formó parte del trabajo desde el principio. Ellos fijaban unas reglas; la máquina las ponía a prueba; los problemas que salían volvían a sus manos, les obligaban a modificar las reglas y daban paso a otra ronda de cálculo. Así estuvieron varios años. El balance final fue de 487 reglas, unos diez mil casos locales examinados a mano y cerca de dos mil configuraciones verificadas una por una por el ordenador. Había configuraciones que exigían noventa minutos en la máquina más lenta y todavía treinta en la más rápida. El total rondó las mil doscientas horas de máquina. Según sus propias cuentas, en ese tiempo se habían efectuado unos diez mil millones de decisiones lógicas. Para el último tramo consiguieron horas en un gran ordenador que la Universidad de Illinois acababa de comprar, en marzo de 1976, para sus tareas administrativas.

Tampoco todo el trabajo manual lo hicieron sus cuatro manos. La versión definitiva de las reglas se dedujo a mano. Durante varios meses de la primera mitad de 1976, Appel, Haken y Dorothea, la hija de Haken, repasaron una a una las 1936 configuraciones que acabarían formando la lista. Dorothea pasó aquellos años entre la enseñanza secundaria y la universidad; más tarde sería investigadora en informática. Antes de hacer pública la demostración, las dos familias reclutaron a cinco de sus hijos: Dorothea y Armin Haken, y Laurel, Peter y Andrew Appel. Comparaban las hojas impresas por la máquina con los dibujos del artículo, página a página, para comprobar que no hubiera errores de copia. Laurel, la hija de Appel, tenía trece años y se encargó de unas setecientas páginas. Haken recordó después, en sustancia, que había trabajado un mes entero y localizado unos ochocientos errores. Ochocientos en setecientas páginas no le parecían muchos. Ella sola corrigió seiscientos cincuenta; para arreglar los restantes, a él y a Appel les bastaron cinco días.

La lista no dejó de cambiar. Las 1936 configuraciones de la prepublicación se redujeron a 1482 en la versión publicada y, en revisiones posteriores, a unas 1405. El artículo apareció en dos partes en 1977. John Koch también participó en la parte dedicada a la verificación. Lo acompañaban unas cuatrocientas cincuenta páginas en microfichas, llenas de dibujos y registros de comprobación. Appel y Haken hicieron su propia estimación: revisar todo lo que imprimía la máquina para una sola configuración difícil podía costarle a una persona varios años de trabajo a cuarenta horas semanales. Más de una década después, en 1989, publicaron la demostración completa en forma de libro.

En otoño de 1976, el departamento de matemáticas de la Universidad de Illinois modificó su máquina de franquear. Cada carta que salía del departamento llevaba estampada una línea: cuatro colores bastan.

4. Una lista

La máquina comprobaba los elementos de una lista, uno por uno. Para entender qué era aquella lista y por qué resultaba imprescindible hay que volver a la forma del argumento de Kempe: la demostración de 1976 y la de 1879 compartían el mismo esqueleto. Supongamos que cuatro colores no bastan. Entonces tiene que existir un contraejemplo mínimo: de todos los mapas que necesitan cinco colores, el que tiene menos regiones. A continuación hacen falta dos cosas. La primera es una lista de configuraciones locales y la demostración de que en cualquier mapa aparece por fuerza alguna de ellas. Se dice que la lista es inevitable. Para demostrarlo se utiliza el método de descarga: se asigna a cada región un número según cuántas vecinas tenga y después, siguiendo ciertas reglas, se trasladan esas cantidades de unas regiones a otras adyacentes. Al terminar queda necesariamente algún número positivo; allí tiene que haber una de las configuraciones de la lista. La segunda tarea consiste en demostrar que ninguna de esas configuraciones puede aparecer en el contraejemplo mínimo. Si apareciera una, se podría reducir, obtener un mapa más pequeño y colorearlo con cuatro colores, pues por hipótesis ya sabemos hacerlo para los mapas menores. Al reponer la parte reducida, todavía sería posible reajustar los colores. Esta propiedad se llama reducibilidad. Juntas, las dos cosas cierran la trampa: el contraejemplo mínimo está obligado a contener algo que no puede contener. Por tanto, no existe. Appel y Haken habían recibido de Heesch el método de descarga.

La lista de Kempe era muy corta. Primero demostraba que todo mapa contiene al menos una región con cinco vecinas o menos. Su técnica de intercambio resolvía los casos de cuatro vecinas o menos. El caso de cinco era precisamente donde Heawood había encontrado el fallo.

El camino posterior consistió en desmenuzar aquel caso de cinco vecinas y sustituirlo por configuraciones más grandes y más detalladas, hasta poder demostrar por separado que cada una era reducible. Cuanto más fino era el desglose, más larga se volvía la lista y más pesaba la comprobación de cada elemento. Una configuración está rodeada por un anillo de regiones; hay que ensayar todas las maneras de distribuir los cuatro colores por ese anillo y comprobar si se pueden reajustar. Con catorce regiones en el anillo, las distribuciones rozan las doscientas mil. Con dieciocho, superan los dieciséis millones.

Por eso Appel y Haken necesitaban una máquina. No era una cuestión de preferencias. Desde Kempe, la estructura del argumento dejaba dos caminos: encontrar una lista corta o comprobar, uno por uno, todos los elementos de una larga. En cien años, nadie había encontrado la corta.

5. Tres motivos de inquietud

Con el tiempo, la inquietud que se había oído en Toronto se descompuso en tres objeciones. Conviene no confundirlas.

La primera decía: esto no es una demostración. Su formulación más célebre fue la del filósofo Thomas Tymoczko, en 1979. No afirmaba que el teorema de los cuatro colores fuera probablemente falso. Sostenía que una demostración cumplía dos funciones: convencernos de la conclusión y permitirnos recorrer el argumento entero, de principio a fin, para ver por qué era cierto. A esta segunda propiedad le dio un nombre que aludía a la posibilidad de abarcarlo: poder contemplar la demostración completa desde un mismo lugar. La de 1976 cumplía la primera función y había perdido la segunda. Si un cálculo imposible de abarcar de ese modo también recibía el nombre de demostración, el significado de la palabra ya se había ampliado.

La segunda decía: sí, es una demostración, pero no es hermosa. No explica por qué han de bastar precisamente cuatro colores. Muchos de los presentes en Toronto esperaban que algún día apareciera una demostración breve que hiciera visible la razón.

La tercera era la más práctica: quizá sea una demostración, pero no podemos comprobar que esté libre de errores. ¿Funcionaba bien el programa? ¿Faltaba algo en la lista? ¿Se había procesado mal alguno de los miles de resultados? ¿Se habían desalineado los datos impresos durante su transmisión? Aquel mismo año, De Millo, Lipton y Perlis publicaron un artículo donde sostenían que la fiabilidad de una demostración nunca procede solo de su deducción formal. También la produce todo lo que le sucede al entrar en la comunidad matemática: las críticas, las simplificaciones, los nuevos usos y la enseñanza. Si nadie puede revisar una demostración entera, ¿por dónde empieza ese proceso?

Lo que vino después solo dio una respuesta efectiva a la tercera objeción. En los años noventa, Robertson, Sanders, Seymour y Thomas se propusieron revisar la demostración de Appel y Haken. Pronto desistieron. Según explicaron más tarde, una parte se había hecho por ordenador y no podía comprobarse a mano; la parte que supuestamente sí se podía comprobar a mano era de una complejidad y una minuciosidad extraordinarias. Solo introducir una por una las descripciones de más de mil configuraciones ya era una tarea enorme. Decidieron rehacer el trabajo. En 1996 lo consiguieron: redujeron la lista a 633 configuraciones y las reglas de descarga, de varios cientos a treinta y dos. Publicaron los programas y los datos para que otros pudieran repetir la ejecución. Según sus cálculos, revisar a mano la parte que demostraba la inevitabilidad exigía varios meses; con un ordenador, unos veinte minutos. La máquina seguía allí, pero por primera vez su parte del trabajo se había convertido en algo que otra persona podía verificar por separado. En 2005, Gonthier escribió toda esa demostración moderna dentro de un sistema formal, utilizando un programa llamado asistente de demostración, y un núcleo de software muy pequeño fue comprobándola paso a paso. Lo verificado era la vía de 1996, no los programas que Appel y Haken habían ejecutado en 1976. Nadie ha demostrado hasta hoy, mediante ese procedimiento, que aquellos programas originales estuvieran libres de errores. La confianza ya no tenía que depositarse en miles de casos y un largo programa especializado, sino en aquel pequeño núcleo, en las definiciones formales y en el paso que traduce el enunciado original al lenguaje formal. La confianza no desapareció: se redujo, se concentró y quedó al alcance de revisores que podían relevarse unos a otros.

La segunda inquietud sigue sin respuesta. En marzo de 2026, seis autores propusieron en una prepublicación una nueva demostración y un método de coloración mucho más rápido, basado en 8202 configuraciones reducibles, entre ellas dos casos sencillos. A fecha de 1 de octubre de 2026, corresponde hablar de una nueva demostración propuesta por sus autores, y no de una conclusión ya respaldada por un consenso fruto de una larga verificación independiente. Esa cautela tampoco equivale a declararla errónea. Thomassen, uno de los participantes, dijo que lo que quería era una demostración sin ordenador. Nunca había dejado de pensar en ello.

6. Un teorema que no cabe en un libro

El segundo ejemplo es más grande. Tan grande que no cabe en un libro.

En el episodio anterior vimos una estructura: sus elementos se pueden componer de dos en dos, uno de ellos no hace nada y cada uno puede deshacerse. Los matemáticos la llaman grupo. Para descomponerla se utilizan subgrupos normales y los correspondientes grupos cociente. Un grupo es simple si no tiene subgrupos normales propios no triviales; eso no significa que carezca de subgrupos no triviales. Los grupos simples ocupan un lugar parecido al de los números primos: los enteros se obtienen multiplicando primos y todo grupo finito tiene una serie de composición cuyos factores son grupos simples. Pero esos factores no determinan de manera única cómo se ensambló el grupo original. ¿Cuáles son, entonces, todos los grupos simples finitos?

Los más pequeños son modestos: ciclos con un número primo de elementos. Giremos un pentágono regular de quinto de vuelta en quinto de vuelta. Al quinto giro volvemos al principio; esas cinco rotaciones forman un grupo simple. El primer grupo simple en el que el orden de las operaciones importa tiene sesenta elementos: todas las rotaciones de un icosaedro regular. En el episodio décimo, la ecuación de quinto grado se nos quedaba sin una fórmula general de resolución. Si se sigue el problema hasta el fondo, lo que obstruye el paso es precisamente ese grupo simple de sesenta elementos.

La respuesta es una lista. Contiene varias familias infinitas, cuyos miembros se suceden según un patrón, y veintiséis excepciones sueltas que no pertenecen a ninguna de esas familias. La mayor acabó llamándose el Monstruo. El número de sus elementos tiene cincuenta y cuatro cifras. Fischer y Griess predijeron su existencia hacia 1973. El 14 de enero de 1980, en Ann Arbor, Griess anunció que había logrado construirlo: era el conjunto de todas las simetrías de un objeto de 196 883 dimensiones. Al publicar su trabajo, en 1982, lo llamó el gigante amistoso.

Antes de eso, los artículos individuales ya habían empezado a crecer. En 1963, Feit y Thompson demostraron que todo grupo finito de orden impar es resoluble y, por tanto, que cualquier grupo simple finito no conmutativo tiene orden par. El artículo ocupaba 255 páginas: un número entero de una revista. Mucho después, un equipo dirigido por Gonthier incorporó la demostración completa a un asistente de demostración. El trabajo se publicó en 2013.

Demostrar que la lista está completa es demostrar el teorema de clasificación de los grupos simples finitos. No es un artículo ni un libro. Son cientos de artículos, alrededor de un centenar de autores principales y unas diez mil páginas de demostración. Si se suman los resultados previos necesarios, una estimación habitual llega a quince mil. No hay un criterio único para hacer esa cuenta, porque ni siquiera está claro dónde termina esta demostración.

A comienzos de los años ochenta, Daniel Gorenstein publicó un libro cuyo título venía a decir Grupos simples finitos: introducción a su clasificación. Resumía más de veinte años de trabajo como un conjunto ya terminado. Durante todo ese tiempo, Gorenstein había mantenido la visión de conjunto y marcado el rumbo. Años después, Aschbacher, uno de los matemáticos más profundamente implicados, escribió al volver la vista atrás que la opinión general de la comunidad era que la clasificación había quedado completada hacia 1980.

La palabra «completada» no salió de una frase pronunciada por alguien, cierto día, desde un estrado. Nombraba el proceso por el que un programa de investigación se había convertido poco a poco en un resultado aceptado. Se creía que todas las grandes ramas estaban cubiertas y que los especialistas correspondientes sabían resolver lo que quedaba.

Que los especialistas sepan cómo terminar un trabajo y que exista una demostración completa, publicada y citable paso por paso son dos cosas distintas. Entre ambas se escondía el problema.

7. La pieza que faltaba

Una rama entera del árbol de clasificación correspondía a los llamados grupos cuasidelgados. En el proyecto de primera generación, esa parte estaba a cargo de Geoff Mason. En 1980 anunció su clasificación y en 1981 dejó un manuscrito de unas ochocientas páginas que no llegó a publicarse. Solo después se vio con claridad que estaba incompleto y contenía una laguna grave.

No hay una fecha que marque el descubrimiento de esa laguna. No sucedió como en 1890, cuando Heawood pudo señalar un paso concreto de Kempe y decir: aquí está el error. Fue haciéndose evidente poco a poco. Desde finales de los ochenta y a lo largo de los noventa, al reorganizar la demostración de la clasificación, resultó cada vez más difícil dar aquella parte por cerrada. Algo que todos creían terminado desde hacía tiempo no estaba realmente terminado.

La completaron Aschbacher y Stephen Smith. En 2004 publicaron La clasificación de los grupos cuasidelgados, dos volúmenes que sumaban unas mil doscientas veinte páginas. No era una hoja de erratas: era una obra nueva. Después aparecieron algunas omisiones menores, que también fueron subsanadas una a una.

De modo que hay tres afirmaciones que podemos dar por seguras. A comienzos de los años ochenta, la comunidad matemática ya aceptaba la lista como correcta. En la bibliografía pública de la demostración de primera generación faltaba, efectivamente, una parte importante. Los dos volúmenes de 2004 ofrecieron para esa parte un tratamiento completo y publicable.

Gorenstein había comprendido muy pronto que, aun siendo correcta, la primera demostración no tenía una forma final satisfactoria. Con Richard Lyons y Ronald Solomon inició un proyecto de segunda generación: reescribir la demostración dispersa en cientos de artículos como una colección sistemática de monografías, tan autosuficiente como fuera posible y con las dependencias entre resultados claramente establecidas. Gorenstein murió en agosto de 1992. El primer volumen de la segunda generación no salió hasta 1994. La editorial describía el propósito de la colección como una demostración cuidadosa y en buena medida autosuficiente. El décimo volumen apareció en 2023; la reescritura ha continuado desde entonces, de modo que las cifras exactas de volúmenes y páginas deben actualizarse con los registros de publicación. Lyons y Solomon trabajan en la última parte de la línea principal. En Alemania, Stroth tiene además un voluminoso manuscrito dedicado al tramo final. Los doce volúmenes y cinco mil páginas calculados al principio parecen ya un espacio muy ajustado.

¿Ha leído alguien la demostración de primera generación, junto con todos los resultados de los que depende, de principio a fin y línea por línea? No se encuentra a nadie que diga haberlo hecho. Aschbacher, Lyons y Solomon poseen un dominio extraordinario de la estructura completa, y cada zona tiene a sus especialistas. Pero conocer la estructura y comprobar página a página cientos de artículos son trabajos de órdenes de magnitud distintos.

La comunidad matemática no ha resuelto el problema buscando un superlector. Los especialistas de cada zona responden de su parte. Un artículo recurre a otro una y otra vez; cada uso ofrece una ocasión de revisar, aunque una cita no garantice que alguien haya vuelto a comprobar todas las líneas. Cuando aparece una laguna grande, se reescribe. Y las exposiciones de conjunto y las monografías de segunda generación intentan sustituir, en la medida de lo posible, la pregunta de quién confía en quién por otra: qué resultado depende de cuál. Que un teorema se conozca no significa que una persona conozca todos sus detalles.

8. Tres maneras de terminar

Hay un tercer ejemplo. En 1611, Kepler escribió un librito sobre los copos de nieve hexagonales como regalo de Año Nuevo para su mecenas. De paso, aventuró una conjetura: la disposición que forman las naranjas de una frutería cuando se apilan por capas hasta hacer una pirámide ya es la más densa posible en el espacio. El origen del problema estaba en las balas de cañón. Walter Raleigh había pedido a su ayudante Harriot que encontrara una manera de contar las de una pila, y Harriot mantenía correspondencia con Kepler desde 1606. En 1900, Hilbert incluyó la cuestión en el problema decimoctavo de su lista. Thomas Hales anunció una demostración en 1998. Una mitad consistía en razonamientos tradicionales; la otra, en verificar multitud de desigualdades, resolver problemas de programación lineal y efectuar enumeraciones finitas. Su alumno Samuel Ferguson hizo una aportación decisiva en una de las partes clave.

Annals of Mathematics reunió un equipo de unos doce evaluadores, que dedicaron cerca de cuatro años a revisar el trabajo. En 2003, su responsable, Fejes Tóth, dijo que estaban seguros al noventa y nueve por ciento de que la demostración era correcta, pero que no podían certificar todos los cálculos. La cifra se ha repetido incontables veces desde entonces. Ponía un número a algo que la evaluación por pares suele dejar sin decir: revisar un artículo nunca ha sido accionar un interruptor con solo dos posiciones, correcto o incorrecto. En 2005, Annals of Mathematics publicó el argumento principal, de la página 1065 a la 1185, ciento veintiuna en total. Los recursos computacionales y los artículos relativos a los cálculos se facilitaron o publicaron por separado.

Hales no se detuvo ahí. Puso en marcha un proyecto para llevar la demostración entera a un sistema formal y dejar que un pequeño núcleo de software la comprobara. Así ya no habría que pedirle a ningún evaluador que confiara en aquellos cálculos. El 10 de agosto de 2014 se anunció la conclusión del proyecto, que había utilizado dos asistentes de demostración. La demostración formal apareció publicada en 2017, con veintidós firmas.

Un mismo teorema, tres fechas y tres sentidos de la palabra «terminado». En 1998, el autor consideró que había acabado. En 2005, la revista juzgó el resultado lo bastante fiable para publicarlo. En 2014, un núcleo formal terminó de comprobarlo.

Es la cuarta vez que esta serie tropieza con la pregunta. En el tercer episodio nos preguntábamos si aquel libro contaba como el comienzo de la axiomatización; en el quinto, si aquellos comentarios contaban como demostraciones; en el noveno, si aquellas series contaban como cálculo infinitesimal. Las tres veces se discutía qué nombre darle a algo, y quienes lo discutían eran los que habían venido después. Aquí cambia la pregunta. La cosa está delante y nadie disputa su nombre. Lo que se discute es si podemos decir que se conoce. Y quienes lo preguntan son sus contemporáneos: al salir de la sala de Toronto en 1976, los matemáticos ya expresaban su inquietud. Tres años después, Tymoczko la convirtió en un problema escrito.

La voz contraria tampoco ha dejado de oírse. En 1980, Krakowski respondió a Tymoczko que toda demostración formal de longitud finita puede, en principio, abarcarse por completo: la humanidad solo necesita aprender a vivir un poco más. Había ironía en la frase, pero también una razón muy firme. Las matemáticas nunca han exigido que todos los antecedentes de una demostración quepan a la vez en una sola cabeza. Un artículo de veinte páginas puede apoyarse en teoremas repartidos por miles de páginas de libros, y nadie le niega por eso la condición de demostración. En 1994, Thurston escribió que los matemáticos buscan maneras de que las personas comprendan las matemáticas y piensen con ellas. Desde esa perspectiva, una demostración debe hacer algo más que garantizar la verdad de una conclusión: ha de poner algo en manos de quien la lee. El problema de las grandes demostraciones no es que nadie posea el conjunto; tampoco en las matemáticas corrientes lo posee nadie. El problema es que la cadena de confianza se vuelve muy larga. Una buena respuesta consiste en hacer cada eslabón lo más pequeño posible y en permitir que distintas personas se releven para comprobarlo.

Por eso, el cambio real desde 1976 hasta hoy no consiste en que las matemáticas hayan pasado de las manos humanas a las máquinas. Por primera vez, a gran escala, se han separado tres cosas que solían ir juntas: que un argumento sea válido, que permita comprender y que pueda comprobarse en la práctica. El teorema de los cuatro colores dejó el cálculo fuera del campo de visión de una sola persona; el teorema de clasificación hizo lo mismo con la bibliografía y los conocimientos especializados. La formalización intenta reunir de nuevo todo eso en un objeto que una máquina pueda verificar paso a paso. Responde a una gran parte de la pregunta de por qué tenemos derecho a confiar. La otra parte sigue ahí: cuando una comunidad matemática sabe de manera fiable que algo es cierto, ¿significa eso que también entiende por qué lo es?

Lo que una sola persona no puede abarcar puede dividirse en partes que alguien sí pueda tener entre las manos.

En 1977, tres jóvenes del MIT hicieron público un método de cifrado basado en una dificultad matemática: multiplicar dos números primos grandes es fácil; recuperar los dos factores a partir del producto es difícil. Cinco años después, el método tenía una empresa. Al sexto, una patente.

Seguimos echando cuentas; qué cuenta como matemáticas sigue siendo una cuenta pendiente.

Fuentes y lecturas complementarias

Las referencias siguientes corresponden a los detalles históricos y a las discrepancias de interpretación del texto. Los registros de las colecciones, la literatura antigua y las reconstrucciones modernas no son pruebas del mismo tipo.

• Prepublicación de 2026 sobre los cuatro colores y la coloración en tiempo casi lineal
• Anuncio de investigación de 1996 sobre la nueva demostración de los cuatro colores
• Gonthier: demostración formal del teorema de los cuatro colores
• Artículo original sobre la demostración del teorema del orden impar verificada por ordenador
• La clasificación de los grupos cuasidelgados: obra original
• Hales: artículo original sobre la conjetura de Kepler en Annals of Mathematics
• Demostración formal de la conjetura de Kepler de 2017