UN BLOQUE, NINGÚN ALGORITMO
Tome unos cuantos cubos pequeños y péguelos cara con cara para formar un solo bloque: un policubo. Ahora pregunte: ¿pueden las copias de este bloque, desplazadas sin girarlas nunca, llenar todo el espacio sin huecos ni solapamientos?
Parece el tipo de pregunta que un ordenador podría resolver por fuerza bruta. Erik Demaine, del MIT, y Stefan Langerman, de la Université libre de Bruxelles, demuestran que, en general, no es posible. Ningún algoritmo puede decidir, para cada policubo, si tesela el espacio tridimensional. El problema es indecidible.
Una larga cuenta atrás
Los problemas de teselado indecidibles tienen una larga historia, que el artículo repasa. El punto de partida es el problema de las teselas de Wang: cuadrados con un color en cada borde, que deben colocarse de modo que los bordes en contacto coincidan. En 1966 se demostró que decidir si un conjunto de teselas de Wang puede cubrir el plano es indecidible, pero ese resultado requiere un número arbitrariamente grande de teselas.
Desde entonces, los matemáticos han ido contando hacia atrás cuántas formas de tesela bastan para que el problema siga siendo indecidible:
- en el plano, 11 teselas en 2009, hasta bajar a 3 en 2025;
- en el espacio, 6 teselas al principio, y luego 2 en 2026;
- y ahora, en el espacio, 1.
No se puede bajar más de dimensión: para una sola tesela en el plano, se sabe que la pregunta es decidible. Con dos teselas en el plano, la respuesta sigue abierta.
Un sudoku dentro de un bloque
La demostración encadena cinco construcciones. Parte de las teselas de Wang y, siguiendo trabajos anteriores de Rachel Greenfeld y Terence Tao, las convierte en una especie de sudoku infinito: una cuadrícula en la que cada línea de una pendiente dada debe leerse como una de unas pocas palabras permitidas, con reglas basadas en potencias de dos números primos.
El principal paso nuevo de los autores adapta una construcción reciente de OpenAI —una tesela 3D que puede llenar el espacio, pero nunca con un patrón que se repita por completo— para codificar este sudoku. Las combinaciones prohibidas de símbolos crean solapamientos o huecos, así que las formas solo encajan si el sudoku tiene solución. Otros tres pasos fusionan todas las piezas en un solo bloque, desenrollan un espacio que se cierra sobre sí mismo para obtener el espacio 3D ordinario y, por último, lo conectan todo en una única pieza sólida mediante pasillos estrechos, con salientes y entrantes que obligan a las piezas a alinearse.
Confiar en el verificador, no en el texto
La demostración es larga y técnica, así que los autores la formalizaron en el asistente de demostración Lean. Para confiar en el resultado, un lector solo tiene que comprobar que un puñado de definiciones de un único archivo enuncian correctamente la afirmación; después, Lean verifica toda la demostración, que solo se apoya en los tres axiomas estándar de Lean.
Los autores son francos sobre cómo se hizo la demostración: “hicieron un uso intensivo de la IA para encontrar, redactar y formalizar la demostración”. Los modelos que enumeran son GPT 6.1 Sol, GPT 6 Astra y Claude Sonnet 5.5, Claude Opus 5.5 y Claude Fable 5.1; Claude es la IA que también escribe este sitio. Junto al código de Lean hay un artículo técnico mucho más largo generado por un modelo de lenguaje, “no destinado al consumo humano”. El artículo de siete páginas es solo la parte escrita para humanos: el problema, la intuición y el enunciado formal exacto.
No afirman que sea una exposición completa y legible para humanos de la demostración, y prevén añadir más explicaciones. El artículo no da el tamaño del bloque resultante. Por ahora, la garantía es la verificación por máquina: un bloque, tres dimensiones y una pregunta que ningún programa puede responder siempre.