Los ordenadores hacen posibles demostraciones matemáticas más largas de lo que un humano puede escribir en muchas vidas. La más larga ocupa 200 terabytes (Tb), unos 200 millones de millones de caracteres; el récord anterior era una prueba de 13 Tb obtenida en 2014. Se ha demostrado que el problema del coloreado de ternas pitagóricas no tiene solución para n=7825; además, se han encontrado todas las soluciones del problema para n=7824. Este problema se ha resuelto usando el supercomputador Stampede de la Universidad de Texas.

El problema resuelto consiste en saber si es posible colorear los números de 1 hasta n en dos colores (rojo y azul) de tal forma que no haya ninguna terna pitagórica con los tres números del mismo color; una terna pitagórica (a,b,c) cumple que a²+b²=c². No hay una solución única, por lo que se usa el color blanco para colorear los números que pueden ser coloreados en rojo o en azul sin afectar al resultado. Por ejemplo, para la famosa terna (3,4,5), si se colorean en azul 3 y 4, entonces 5 debe ser rojo. En la figura 3 es azul, 5 es rojo y 4 puede ser azul o rojo.

El artículo es Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek, «Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer,» SAT 2016, Lecture Notes in Computer Science 9710: 228-245 (2016), doi: 10.1007/978-3-319-40970-2_15, arXiv:1605.00723 [cs.DM]. Más información en Evelyn Lamb, «Two-hundred-terabyte maths proof is largest ever,» Nature 534: 17-18 (02 Jun 2016), doi: 10.1038/nature.2016.19990.

Una búsqueda sistemática de posibles soluciones es imposible, ya que habría que explorar unas 10²³⁰⁰ posibilidades.Usando técnicas que aprovechan la simetría del problema, la demostración final ha exigido explorar menos de un billón de posibilidades. Aún así, ha tomado más de dos días a los 800 procesadores del superordenador Stampede. Una vez obtenida la solución general ha sido verificada por otro ordenador de forma independiente.

Para un matemático este tipo de demostraciones por ordenador son poco atractivas, ya que no iluminan la razón última por la cual, por ejemplo, el problema para n=7825 no tiene solución. Aún así, hay que aceptar que existen verdades matemáticas cuya demostración solo es posible usando la potencia de cálculo de los superordenadores.