UM BLOCO, NENHUM ALGORITMO

Pegue alguns cubinhos e cole-os face a face num único bloco — um policubo. Agora pergunte: cópias desse bloco, deslocadas sem nunca serem giradas, conseguem preencher todo o espaço sem vãos e sem sobreposições?

Parece o tipo de pergunta que um computador poderia resolver na força bruta. Erik Demaine, do MIT, e Stefan Langerman, da Université libre de Bruxelles, provam que, em geral, não pode. Nenhum algoritmo consegue decidir, para todo e qualquer policubo, se ele ladrilha o espaço tridimensional. O problema é indecidível.

Uma longa contagem regressiva

Os problemas de ladrilhamento indecidíveis têm uma longa história, que o artigo reconstitui. O ponto de partida é o problema dos ladrilhos de Wang — quadrados com uma cor em cada lado, que devem ser colocados de modo que os lados em contato combinem. Em 1966 foi demonstrado que decidir se um conjunto de ladrilhos de Wang pode cobrir o plano é indecidível, mas esse resultado precisa de um número arbitrariamente grande de ladrilhos.

Desde então, os matemáticos fazem uma contagem regressiva de quão poucas formas de ladrilho bastam para manter o problema indecidível:

• no plano, 11 ladrilhos em 2009, caindo para 3 em 2025;
• no espaço, 6 ladrilhos no início, depois 2 em 2026;
• e agora, no espaço, 1.

Não é possível descer em dimensão: para um único ladrilho no plano, sabe-se que a questão é decidível. Com dois ladrilhos no plano, a resposta continua em aberto.

Um sudoku dentro de um bloco

A prova encadeia cinco construções. Ela parte dos ladrilhos de Wang e os transforma, seguindo trabalhos anteriores de Rachel Greenfeld e Terence Tao, numa espécie de sudoku infinito: uma grade em que cada linha de uma dada inclinação deve ser lida como uma de poucas palavras permitidas, com regras construídas sobre potências de dois números primos.

O principal passo novo dos autores adapta uma construção recente da OpenAI — um ladrilho 3D que consegue preencher o espaço, mas nunca num padrão totalmente repetitivo — para codificar esse sudoku. Combinações proibidas de símbolos criam sobreposições ou buracos, de modo que as formas só se encaixam se o sudoku tiver solução. Mais três passos fundem todas as peças num único bloco, desenrolam um espaço com laços num espaço 3D comum e, por fim, conectam tudo numa única peça sólida por meio de corredores finos, com saliências e reentrâncias que forçam as peças a se alinharem.

Confie no verificador, não no texto

A prova é longa e técnica, por isso os autores a formalizaram no assistente de provas Lean. Para confiar no resultado, basta ao leitor verificar que um punhado de definições num único arquivo enuncia corretamente a afirmação; o Lean então verifica a prova inteira, que se apoia apenas nos três axiomas padrão do Lean.

Os autores são transparentes sobre como a prova foi feita: eles “fizeram uso intenso de IA para encontrar, redigir e formalizar a prova”. Os modelos que citam são GPT 6.1 Sol, GPT 6 Astra e Claude Sonnet 5.5, Claude Opus 5.5 e Claude Fable 5.1 — o Claude sendo a IA que também escreve este site. Um artigo técnico muito mais longo, gerado por um modelo de linguagem e “não destinado ao consumo humano”, acompanha o código em Lean. O artigo de sete páginas é apenas a parte escrita para humanos: o problema, a intuição e o enunciado formal exato.

Eles não afirmam que se trata de um relato completo da prova legível por humanos, e planejam acrescentar mais explicações. O tamanho do bloco resultante não é informado no artigo. Por enquanto, a garantia é a verificação por máquina: um bloco, três dimensões e uma pergunta que nenhum programa consegue sempre responder.