Conjectura de Kepler - Kepler conjecture

A conjectura de Kepler , em homenagem ao matemático e astrônomo do século 17 Johannes Kepler , é um teorema matemático sobre o empacotamento de esferas no espaço euclidiano tridimensional . Afirma que nenhum arranjo de espaços de preenchimento de esferas de tamanho igual tem uma densidade média maior do que a do empacotamento cúbico cúbico ( cúbico de face centrada ) e arranjos de empacotamento hexagonal fechado . A densidade desses arranjos é de cerca de 74,05%.

Em 1998, Thomas Hales , seguindo uma abordagem sugerida por Fejes Tóth (1953) , anunciou que tinha uma prova da conjectura de Kepler. A prova de Hales é uma prova por exaustão envolvendo a verificação de muitos casos individuais usando cálculos complexos de computador. Os árbitros disseram que estavam "99% certos" da correção da prova de Hales, e a conjectura de Kepler foi aceita como um teorema . Em 2014, a equipe do projeto Flyspeck, liderada por Hales, anunciou a conclusão de uma prova formal da conjectura Kepler usando uma combinação dos assistentes de prova Isabelle e HOL Light . Em 2017, a prova formal foi aceita pela revista Forum of Mathematics, Pi .

Fundo

Diagramas de embalagem fechada cúbica (esquerda) e embalagem fechada hexagonal (direita).

Imagine encher um grande recipiente com pequenas esferas de tamanhos iguais: digamos, uma jarra de galão de porcelana com bolas de gude idênticas. A "densidade" do arranjo é igual ao volume total de todos os mármores, dividido pelo volume da jarra. Maximizar o número de berlindes no jarro significa criar um arranjo de berlindes empilhados entre as laterais e o fundo do jarro, que tenha a maior densidade possível, de modo que os berlindes sejam embalados o mais próximo possível.

A experiência mostra que soltar as bolas de gude aleatoriamente, sem nenhum esforço para organizá-las de forma justa, atingirá uma densidade de cerca de 65%. No entanto, uma densidade mais alta pode ser alcançada organizando cuidadosamente os mármores da seguinte forma:

  1. Para a primeira camada de mármores, organize-os em uma estrutura hexagonal ( o padrão de favo de mel )
  2. Coloque a próxima camada de mármores nas lacunas mais baixas que você pode encontrar acima e entre os mármores na primeira camada, independentemente do padrão
  3. Continue com o mesmo procedimento de preenchimento das lacunas inferiores da camada anterior, para a terceira e as demais camadas, até que os mármores atinjam a borda superior do jarro.

Em cada etapa, há pelo menos duas opções de como colocar a próxima camada, de modo que esse método não planejado de empilhar as esferas cria um número incontavelmente infinito de embalagens igualmente densas. Os mais conhecidos são chamados de empacotamento cúbico e hexagonal . Cada um desses arranjos tem uma densidade média de

A conjectura do Kepler diz que isso é o melhor que pode ser feito - nenhum outro arranjo de mármores tem uma densidade média maior: Apesar de haver surpreendentemente muitos arranjos diferentes possíveis que seguem o mesmo procedimento das etapas 1-3, sem embalagem (de acordo com o procedimento ou não) pode caber mais bolas de gude no mesmo jarro.

Origens

Um dos diagramas de Strena Seu de Nive Sexangula , ilustrando a conjectura de Kepler.

A conjectura foi declarada pela primeira vez por Johannes Kepler  ( 1611 ) em seu artigo 'Sobre o floco de neve de seis pontas'. Ele havia começado a estudar arranjos de esferas como resultado de sua correspondência com o matemático e astrônomo inglês Thomas Harriot em 1606. Harriot era amigo e assistente de Sir Walter Raleigh , que lhe deu o problema de determinar a melhor forma de empilhar balas de canhão em os conveses de seus navios. Harriot publicou um estudo de vários padrões de empilhamento em 1591 e desenvolveu uma versão inicial da teoria atômica .

Século dezenove

Kepler não tinha uma prova da conjectura, e o próximo passo foi dado por Carl Friedrich Gauss  ( 1831 ), que provou que a conjectura de Kepler é verdadeira se as esferas tiverem que ser arranjadas em uma rede regular .

Isso significava que qualquer arranjo de embalagem que refutasse a conjectura de Kepler teria que ser irregular. Mas eliminar todos os arranjos irregulares possíveis é muito difícil, e é isso que torna a conjectura do Kepler tão difícil de provar. Na verdade, existem arranjos irregulares que são mais densos do que o arranjo de empacotamento cúbico em um volume pequeno o suficiente, mas qualquer tentativa de estender esses arranjos para preencher um volume maior é agora conhecido por sempre reduzir sua densidade.

Depois de Gauss, nenhum progresso foi feito no sentido de provar a conjectura de Kepler no século XIX. Em 1900, David Hilbert incluiu-o em sua lista de vinte e três problemas matemáticos não resolvidos - faz parte do décimo oitavo problema de Hilbert .

Século vinte

O próximo passo em direção a uma solução foi dado por László Fejes Tóth . Fejes Tóth (1953) mostrou que o problema de determinar a densidade máxima de todos os arranjos (regulares e irregulares) poderia ser reduzido a um número finito (mas muito grande) de cálculos. Isso significava que uma prova por exaustão era, em princípio, possível. Como Fejes Tóth percebeu, um computador rápido o suficiente poderia transformar esse resultado teórico em uma abordagem prática para o problema.

Enquanto isso, tentativas foram feitas para encontrar um limite superior para a densidade máxima de qualquer arranjo possível de esferas. O matemático inglês Claude Ambrose Rogers (ver Rogers (1958) ) estabeleceu um valor limite superior de cerca de 78%, e esforços subsequentes de outros matemáticos reduziram esse valor ligeiramente, mas ainda era muito maior do que a densidade de empacotamento cúbico próximo de cerca de 74%.

Em 1990, Wu-Yi Hsiang afirmou ter provado a conjectura de Kepler. A prova foi elogiada pela Encyclopædia Britannica e pela Science e Hsiang também foi homenageado em reuniões conjuntas da AMS-MAA. Wu-Yi Hsiang ( 1993 , 2001 ) afirmou provar a conjectura de Kepler usando métodos geométricos. No entanto, Gábor Fejes Tóth (filho de László Fejes Tóth) afirmou na sua análise do jornal "No que diz respeito aos detalhes, a minha opinião é que muitas das declarações principais não têm provas aceitáveis." Hales (1994) fez uma crítica detalhada do trabalho de Hsiang, à qual Hsiang (1995) respondeu. O consenso atual é que a prova de Hsiang está incompleta.

Prova de Hales

Seguindo a abordagem sugerida por Fejes Tóth (1953) , Thomas Hales, então na Universidade de Michigan , determinou que a densidade máxima de todos os arranjos poderia ser encontrada minimizando uma função com 150 variáveis. Em 1992, auxiliado por seu aluno de graduação Samuel Ferguson, ele embarcou em um programa de pesquisa para aplicar sistematicamente métodos de programação linear para encontrar um limite inferior no valor dessa função para cada um de um conjunto de mais de 5.000 configurações diferentes de esferas. Se um limite inferior (para o valor da função) pudesse ser encontrado para cada uma dessas configurações que fosse maior do que o valor da função para o arranjo de empacotamento cúbico, então a conjectura de Kepler seria provada. Encontrar limites inferiores para todos os casos envolveu a solução de cerca de 100.000 problemas de programação linear.

Ao apresentar o andamento de seu projeto em 1996, Hales disse que o fim estava próximo, mas que poderia levar "um ou dois anos" para ser concluído. Em agosto de 1998, Hales anunciou que a prova estava completa. Nessa fase, consistia em 250 páginas de notas e 3 gigabytes de programas de computador, dados e resultados.

Apesar da natureza incomum da prova, os editores dos Annals of Mathematics concordaram em publicá-la, desde que fosse aceita por um painel de doze árbitros. Em 2003, após quatro anos de trabalho, o chefe do painel de árbitros, Gábor Fejes Tóth, relatou que o júri tinha "99% de certeza" da veracidade da prova, mas não conseguiu atestar a veracidade de todos os cálculos computacionais .

Hales (2005) publicou um artigo de 100 páginas descrevendo em detalhes a parte não computacional de sua prova. Hales & Ferguson (2006) e vários artigos subsequentes descreveram as porções computacionais. Hales e Ferguson receberam o Prêmio Fulkerson por trabalhos de destaque na área de matemática discreta em 2009.

Uma prova formal

Em janeiro de 2003, Hales anunciou o início de um projeto colaborativo para produzir uma prova formal completa da conjectura Kepler. O objetivo era remover qualquer incerteza remanescente sobre a validade da prova, criando uma prova formal que pode ser verificada por um software de verificação automática de prova , como o HOL Light e o Isabelle . Este projeto é denominado Flyspeck - o F, P e K significando Prova Formal de Kepler . Hales estimou que produzir uma prova formal completa levaria cerca de 20 anos de trabalho. Hales publicou pela primeira vez um "projeto" para a prova formal em 2012; a conclusão do projeto foi anunciada em 10 de agosto de 2014. Em janeiro de 2015 Hales e 21 colaboradores enviaram um artigo intitulado "Uma prova formal da conjectura Kepler" à arXiv , alegando ter provado a conjectura. Em 2017, a prova formal foi aceita na revista Forum of Mathematics .

Problemas relacionados

Teorema de Thue
O empacotamento hexagonal regular é o empacotamento circular mais denso do plano (1890). A densidade é π ⁄ √ 12 .
O análogo bidimensional da conjectura de Kepler; a prova é elementar. Henk e Ziegler atribuem esse resultado a Lagrange, em 1773 (ver referências, pág. 770).
Uma prova simples de Chau e Chung de 2010 usa a triangulação de Delaunay para o conjunto de pontos que são centros de círculos em um empacotamento de círculo saturado.
A conjectura hexagonal do favo de mel
A partição mais eficiente do plano em áreas iguais é o ladrilho hexagonal regular.
Relacionado ao teorema de Thue.
Conjectura dodecaédrica
O volume do poliedro de Voronoi de uma esfera em um empacotamento de esferas iguais é pelo menos o volume de um dodecaedro regular com inradius 1. Prova de McLaughlin, pela qual ele recebeu o Prêmio Morgan de 1999 .
Um problema relacionado, cuja prova usa técnicas semelhantes à prova de Hales da conjectura de Kepler. Conjectura de L. Fejes Tóth na década de 1950.
O problema Kelvin
Qual é a espuma mais eficiente em 3 dimensões? Isso foi conjecturado para ser resolvido pela estrutura de Kelvin , e isso foi amplamente acreditado por mais de 100 anos, até ser contestado em 1993 pela descoberta da estrutura de Weaire-Phelan . A descoberta surpreendente da estrutura Weaire-Phelan e a refutação da conjectura de Kelvin é uma razão para a cautela em aceitar a prova de Hales da conjectura de Kepler.
Embalagem de esfera em dimensões superiores
Em 2016, Maryna Viazovska anunciou provas dos pacotes de esfera ideais nas dimensões 8 e 24. No entanto, a questão do pacote de esferas ideal em dimensões diferentes de 1, 2, 3, 8 e 24 ainda está em aberto.
Conjectura de embalagem de Ulam
Não se sabe se existe um sólido convexo cuja densidade de empacotamento ideal é inferior à da esfera.

Referências

Publicações

links externos