A pesquisa no computador ajudou a resolver o problema de matemática de 90 anos

Ao traduzir a hipótese de Keller em uma linguagem de pesquisa gráfica compreensível por computador, os pesquisadores finalmente resolveram o problema de cobrir espaços com ladrilhos







Uma equipe de matemáticos finalmente descobriu a hipótese de Keller - mas não por conta própria. Em vez disso, eles treinaram uma frota inteira de computadores e resolveram o problema.



A hipótese de Keller, formulada há 90 anos por Ott-Heinrich Keller, está relacionada à tarefa de revestir espaços com azulejos idênticos. Ela argumenta que se você pavimentar um espaço bidimensional com ladrilhos quadrados bidimensionais, então pelo menos dois deles terão que tocar os lados completamente, e não parcialmente. A hipótese faz a mesma previsão para quaisquer dimensões - ou seja, ao preencher um espaço de 12 dimensões com "quadrados" de 12 dimensões, pelo menos dois deles devem ter uma borda comum.



Durante anos, os matemáticos lutaram por essa hipótese, provando sua verdade para algumas dimensões e falsa para outras. E no último outono a questão permaneceu sem solução apenas para o espaço de sete dimensões.



Mas novas evidências geradas por computador também resolveram esse problema. A prova , publicada em outubro passado, é um dos mais novos exemplos da combinação de gênio humano e poder de computação absoluto para responder às questões mais emocionantes da matemática.



Os autores do novo trabalho, Joshua Breukensik de Stanford, Marin Hijul e John Mackey da Carnegie Mellon University, e David Narvaez do Rochester Institute of Technology, resolveram esse problema usando 40 computadores. Em apenas 30 minutos, as máquinas deram uma resposta monossilábica: sim, em sete dimensões, a hipótese está correta. E nem mesmo temos que tirar essa conclusão pela fé.



Anexada à resposta está uma longa evidência explicando sua verdade. A prova é muito longa para um ser humano entender, mas outro programa de computador pode verificá-la.



Em outras palavras, mesmo que não saibamos exatamente o que os computadores fizeram para provar a hipótese de Keller, podemos pelo menos ter certeza de que eles fizeram tudo certo.



A misteriosa sétima dimensão



É fácil ver que a conjectura de Keller é verdadeira em duas dimensões. Pegue um pedaço de papel e tente cobri-lo com quadrados iguais, sem lacunas ou sobreposições. Em breve você perceberá que só pode fazer isso se pelo menos dois quadrados tiverem o mesmo lado. Se você tiver cubos em mãos, será fácil para você verificar se a hipótese é verdadeira para a terceira dimensão. Em 1930, Keller sugeriu que essa relação funcionasse para todas as dimensões e seus ladrilhos correspondentes.



Os primeiros resultados apoiaram a previsão de Keller. Em 1940, Oscar Perron provou que a hipótese estava correta para as medidas de um a seis. No entanto, mais de 50 anos depois, uma nova geração de matemáticos encontrou o primeiro contra-exemplo a esta hipótese: em 1992, Jeffrey Lagarias e Peter Shoreprovou que a hipótese não funciona na 10ª dimensão.





A hipótese de Keller prevê que ao preencher um espaço em qualquer dimensão, pelo menos dois ladrilhos devem tocar as laterais completamente.

Ao preencher o espaço bidimensional, muitos ladrilhos têm lados comuns (linhas azuis).

Ao preencher o espaço 3D, muitos cubos têm faces comuns (azul).




É fácil mostrar que se uma hipótese falha em alguma dimensão, ela não vale em todas as dimensões superiores. Portanto, após o trabalho de Lagarias e Shor, resta apenas resolver o problema para a sétima, oitava e nona dimensões. Em 2002, Mackey provou que a hipótese de Keller era falsa para a dimensão oito (e, portanto, nove).



Apenas a sétima dimensão permaneceu aberta - ou era a maior dimensão para a qual essa hipótese é verdadeira ou a menor na qual a hipótese era incorreta.



“Ninguém sabe exatamente o que está acontecendo lá”, disse Khiyul.



Ligue os pontos



Enquanto os matemáticos lutaram com esse problema por várias décadas, seus métodos mudaram gradualmente. Perron trabalhou nas primeiras seis dimensões usando apenas lápis e papel, mas na década de 1990, os pesquisadores descobriram como traduzir a hipótese de Keller em uma forma completamente diferente - permitindo que usassem computadores para resolvê-la.



A formulação original da conjectura de Keller diz respeito ao espaço contínuo e suave. Nesse espaço, há um número infinito de maneiras de colocar um número infinito de peças. Mas os computadores não são bons em resolver problemas com um número infinito de opções - para lidar com eles, eles precisam de objetos discretos e finitos.





Marin Hijul da Carnegie Mellon University



Em 1990, Kereszteli Korradi e Sandor Shabo criaram um objeto discreto adequado. Eles mostraram que questões equivalentes à hipótese de Keller podem ser feitas sobre este objeto. E se você provar algo relacionado a esses objetos, a hipótese de Keller será provada. Isso reduziu a questão do infinito a um problema aritmético menos complexo com vários números.



É assim que funciona.



Digamos que você queira entender a hipótese de Keller em duas dimensões. Corradi e Shabo descobriram um método para isso, usando a construção de uma estrutura, que eles chamaram de gráfico de Keller.



Para começar, imagine que existem 16 dados na mesa, e todos têm uma borda superior com dois pontos (dois pontos denotam um espaço bidimensional e porque existem 16 cubos - veremos um pouco mais tarde). Todos os cubos são girados da mesma maneira, de modo que dois pontos sejam localizados da mesma forma para todos. Pinte cada ponto com uma das quatro cores: vermelho, verde, branco ou preto.



Os pontos em um cubo não mudam de lugar - deixe um deles denotar a coordenada xe o outro - y. Depois de colorir os cubos, começamos a desenhar linhas, ou arestas, entre pares de cubos se duas condições forem satisfeitas: os pontos no mesmo lugar para um par de cubos têm cores diferentes, e no outro eles são diferentes e pareados, e os pares são considerados vermelhos com verdes ou pretos com branco.





Gráfico de Keller para duas dimensões. Encontrar um subconjunto de quatro cubos em que cada um está conectado a todos os outros, você contestará a hipótese de Keller para o espaço bidimensional. No entanto, esse subconjunto não existe e a hipótese está correta.

Abaixo está um exemplo de um clique totalmente mesclado de quatro dados que não está no gráfico.




Ou seja, por exemplo, se um cubo tiver dois pontos vermelhos e o outro tiver dois pontos pretos, eles não estão conectados por uma aresta. Seus pontos nas mesmas posições têm cores diferentes, mas não satisfazem o requisito de cores de emparelhamento. Se um cubo tem pontos vermelhos e pretos, e o outro tem dois pontos verdes, eles são conectados por uma aresta, pois em uma posição eles têm cores emparelhadas (vermelho e verde), e na outra são simplesmente diferentes (preto e verde).



Existem 16 maneiras de colorir dois pontos com quatro cores (portanto, temos 16 cubos). Coloque todas essas 16 possibilidades na sua frente. Conecte todos os pares de cubos que satisfaçam os requisitos. Existem quatro cubos em seu esquema, cada um deles combinado com três outros?



Esse subconjunto de cubos totalmente conectado é chamado de clique. Se você puder encontrar um, irá refutar a hipótese de Keller em duas dimensões. No entanto, você não pode - ele simplesmente não existe. E a ausência de tal clique de quatro cubos significa que a hipótese de Keller é verdadeira para duas dimensões.



Esses cubos não são literalmente as mesmas peças que a hipótese de Keller, no entanto, você pode assumir que cada cubo representa uma peça. Considere as cores atribuídas aos pontos como as coordenadas que colocam o cubo no espaço. E a existência de uma borda é uma descrição de como dois cubos são posicionados em relação um ao outro.



Se as cores dos cubos forem iguais, eles representam ladrilhos igualmente espaçados no espaço. Se não tiverem cores e pares de cores comuns (um tem preto e branco, o outro verde e vermelho), indicam ladrilhos parcialmente sobrepostos - o que não é permitido no preenchimento do espaço. Se dois cubos tiverem um conjunto de cores correspondentes e um conjunto da mesma cor (um vermelho-preto, o outro verde-preto), eles representam ladrilhos com um lado comum.



Finalmente, e o mais importante - se eles têm um conjunto de cores emparelhadas e outro conjunto de cores diferentes - ou seja, se eles estão conectados por uma borda - então os cubos representam ladrilhos que estão em contato uns com os outros, mas ligeiramente deslocados, devido ao qual suas bordas não coincidem completamente ... É essa condição que precisamos estudar. Cubos conectados por uma aresta denotam ladrilhos adjacentes que não têm um lado comum - esse é exatamente o arranjo necessário para refutar a hipótese de Keller.



“Eles devem se tocar, mas não completamente”, disse Khiyul.





Mesma cor - mesmo arranjo.

Cores diferentes, sem pares - sobreposição.

Duas cores emparelhadas e um par igual são o lado comum.

Duas cores emparelhadas e duas diferentes - contato parcial pelos lados.




Dimensionamento



Trinta anos atrás, Corradi e Shabo provaram que os matemáticos poderiam usar um procedimento semelhante para trabalhar com a hipótese de Keller em qualquer dimensão, ajustando os parâmetros do experimento. Para provar a hipótese de Keller em três dimensões, você pode usar 216 cubos com três pontos na borda e, possivelmente, três pares de cores (no entanto, há alguma flexibilidade aqui). Então você precisa procurar oito cubos (2 3 ), completamente conectados entre si, de acordo com as mesmas condições que demos acima.



Em geral, para provar a conjectura de Keller em n dimensões, você precisa usar cubos com n pontos e tentar encontrar um clique de tamanho 2 n entre eles . Pode-se supor que representa uma espécie de super-tile (consistindo em 2 nladrilhos menores) capazes de cobrir todo o espaço n-dimensional.



Se você puder encontrar este superladrilho (que não tem ladrilhos com um lado comum), você pode usar cópias dele para cobrir todo o espaço com ladrilhos sem um lado comum, o que refuta a hipótese de Keller.



“Se tiver sucesso, você pode cobrir todo o espaço com transferência. Um bloco sem ladrilhos comuns se estenderá por todo o piso ”, disse Lagarias, agora na Universidade de Michigan.



Mackey refutou a hipótese de Keller na 8ª dimensão, encontrando um clique de 256 cubos (2 8 ), então faltou lidar com a hipótese na 7ª dimensão, encontrando um clique de 128 cubos (2 7) Encontrar esse clique irá refutar a hipótese de Keller na sétima dimensão. Prove que ele não existe e você provará que a hipótese é verdadeira.



Infelizmente, encontrar um clique de 128 cubos é uma tarefa especialmente difícil. Em trabalhos anteriores, os pesquisadores aproveitaram o fato de que as dimensões 8 e 10 podem, em certo sentido, ser "decompostas" em espaços de dimensão inferior, com os quais é mais fácil trabalhar. E aqui isso não funcionou.



“A sétima dimensão é inconveniente porque 7 é um número primo e você não pode dividi-lo em dimensões de ordem menor”, ​​disse Lagarias. “Portanto, não havia escolha a não ser lidar com a combinatória completa desses gráficos.”



Encontrar um clique de 128 cubos pode ser um desafio para o cérebro sem ajuda - mas esses são os tipos de perguntas que os computadores são bons em responder, especialmente com um pouco de ajuda.



A linguagem da lógica



Para transformar a pesquisa de cliques em uma tarefa que um computador possa realizar, você precisa formulá-la em termos de lógica proposicional . Este é um raciocínio lógico que inclui um conjunto de restrições.



Digamos que vocês três estejam planejando uma festa com amigos. Você está tentando criar uma lista de convidados, mas há conflitos de interesse. Digamos que você queira convidar Alexei ou excluir Kolya. Um de seus amigos quer convidar Kolya, ou Vlad, ou ambos. Outro amigo não quer ligar para Alexei ou Vlad. Com tais restrições, é possível criar uma lista de convidados que satisfaça todos os três?



Em termos de ciência da computação, esse problema é chamado de problema de aceitabilidade. Pode ser resolvido descrevendo a condição na fórmula proposicional. Nesse caso, tem a seguinte aparência, e A, K e B denotam possíveis hóspedes: (A OU NÃO K) E (K OU B) E (NÃO A OU NÃO B).



O computador o calcula substituindo 0 ou 1 em cada variável, 0 é o valor da variável "falso" ou desativado e 1 é "verdadeiro" ou ativado. Substituindo 0 em vez de A, dizemos que Alexei não foi convidado e 1 que ele foi convidado. Nesta fórmula simples, 0 e 1 podem ser substituídos (fazendo uma lista de convidados) de várias maneiras, e é possível que depois de iterar todos eles o computador conclua que é impossível satisfazer todos os interesses. Porém, neste caso, há duas maneiras de substituir 1 e 0 para agradar a todos: A = 1, K = 1, B = 0 (convide Alexey e Kolya) e A = 0, K = 0, B = 1 (convide um Vlad )



O programa de computador que resolve essas afirmações é chamado de solucionador SAT, em que SAT é a abreviação de satisfatibilidade. Ele examina todas as combinações de variáveis ​​e dá uma resposta monossilábica - ou SIM, há uma maneira de satisfazer os requisitos da fórmula, ou NÃO, não é.





John Mackie, da Carnegie Mellon University



"Você está apenas tentando ver se pode atribuir valores verdadeiros e falsos a todas as variáveis ​​para que toda a fórmula seja verdadeira e, se sim, é satisfatória e, se não, não", disse Thomas Hales da Universidade de Pittsburgh.



A questão de encontrar um clique de 128 cubos é um problema semelhante. Também pode ser reescrito como uma fórmula proposicional e fornecido ao solucionador SAT. Comece com muitos dados com 7 pontos cada e 6 cores possíveis. É possível colorir os pontos para que 128 cubos sejam conectados entre si de acordo com certas regras? Em outras palavras, é possível atribuir cores para que o clique apareça?



A fórmula proposicional para a pergunta clicada é bastante longa e contém 39.000 variáveis. Cada um pode receber um de dois valores, 0 ou 1. Como resultado, o número de opções possíveis para organizar valores, ou maneiras de atribuir cores, era 2,39.000 - o que é muito, muito mesmo.



Para encontrar a resposta à pergunta sobre a hipótese de Keller em sete dimensões, o computador teria que verificar todas essas combinações - e excluir todas elas (o que significaria que o clique de tamanho 128 não existe e a hipótese de Keller na sétima dimensão está correta), ou encontrar pelo menos seria uma opção de trabalho (refutando a hipótese de Keller).



“Se você fizer uma iteração simples de todas as possibilidades, encontrará um número de 324 dígitos”, disse Mackey. O computador mais rápido do mundo funcionaria até o fim dos tempos, passando por todas as possibilidades.



No entanto, os autores do novo trabalho descobriram como um computador pode dar uma resposta definitiva sem verificar todas as possibilidades. A chave para isso é a eficiência.



Eficiência oculta



Mackey se lembra do dia em que, do seu ponto de vista, o projeto realmente começou a funcionar. Ele estava em frente a um quadro-negro em seu escritório na Carnegie Mellon University, discutindo um problema com dois co-autores, Hijul e Breikensik, quando Hijul propôs uma maneira de estruturar a pesquisa para que pudesse ser concluída em um período de tempo razoável.



“Havia um verdadeiro gênio humano trabalhando em meu escritório naquele dia”, disse Mackey. - Eu era como assistir Wayne Gretzky ou LeBron James nas finais da NBA. Eu tenho arrepios apenas com a lembrança disso. "



Você pode personalizar pesquisas para um gráfico Keller específico de maneiras diferentes. Imagine que você tem muitos cubos em sua mesa e está tentando resolver 128 deles, seguindo as regras do Conde Keller. Digamos que você escolheu 12 corretamente, mas não consegue descobrir como adicionar o próximo. Neste ponto, você pode descartar qualquer configuração de 128 dados que inclua esta configuração não funcional de 12.



“Se você sabe que suas cinco primeiras atribuições não correspondem, não é necessário procurar outras variáveis ​​e isso geralmente diminui muito o campo de pesquisa”, disse Shore, agora no MIT.



Outro tipo de eficiência está associado à simetria. Objetos simétricos são quase os mesmos. A identidade nos permite entender o objeto inteiro como um todo, estudando apenas uma parte dele - olhando para metade do rosto de uma pessoa, você pode restaurá-lo inteiramente.



Da mesma forma, você pode cortar atalhos no caso dos gráficos de Keller. Imagine novamente que você está tentando alinhar os cubos na mesa. Digamos que você comece no centro da mesa e construa sua mão à esquerda. Você lança quatro dados e chega a um beco sem saída. Agora você eliminou uma combinação inicial e todas as combinações baseadas nela. No entanto, você pode excluir o espelhamento dessa combinação inicial - a configuração dos cubos que você obtém se os posicionar da mesma forma, apenas à direita.



“Se você descobriu uma maneira de resolver problemas satisfatórios que habilmente leva em conta a simetria, você simplificou muito a tarefa”, disse Hales.



Quatro colegas tiraram proveito da eficiência dessa busca de uma nova maneira - em particular, eles automatizaram a consideração de casos simétricos, enquanto os matemáticos os processavam quase manualmente.



Como resultado, eles melhoraram tanto a busca por cliques de tamanho 128 que, em vez de verificar 2,39.000 configurações, seu programa teve que verificar apenas cerca de um bilhão ( 2,30 ). Isso fez uma busca que poderia levar uma eternidade em uma tarefa por uma manhã. Finalmente, depois de apenas meia hora de cálculos, eles receberam uma resposta.



“Os computadores disseram não, então sabemos que a hipótese funciona”, disse Hiyul. É impossível colorir os 128 cubos de modo que todos se fundam, então a hipótese de Keller para a sétima dimensão é confirmada. Para qualquer colocação de ladrilhos cobrindo um espaço, haverá inevitavelmente pelo menos um par de bordas que se tocam completamente.



O computador não deu apenas uma resposta monossilábica. Ele anexou a ele uma longa prova de 200 GB apoiando esta conclusão.



A prova não é apenas um cálculo de todos os conjuntos de variáveis ​​que foram verificados por um computador. Este é um argumento lógico que prova que o clique necessário não pode existir. Os pesquisadores alimentaram as evidências em um programa que testa as evidências formais, rastreando a lógica do argumento e validando-a.



“Não passamos por todas as opções e não encontramos nada. Analisamos todas as opções e conseguimos anotar a prova de que tal coisa não existe, - disse Mackey. "Fomos capazes de anotar evidências de insatisfação."



All Articles