Onde e como os computadores ajudaram a provar um teorema?

55

O objetivo desta pergunta é coletar exemplos da ciência da computação teórica em que o uso sistemático de computadores foi útil

  1. na construção de uma conjectura que leva a um teorema,
  2. falsificar uma abordagem de conjectura ou prova,
  3. construir / verificar (partes de) uma prova.

Se você tem um exemplo específico, descreva como foi feito. Talvez isso ajude outras pessoas a usar computadores com mais eficiência em suas pesquisas diárias (o que ainda parece ser uma prática bastante incomum no TCS atualmente).

(Marcado como wiki da comunidade, pois não há uma resposta "correta").

Moritz
fonte
Devo dizer que estou particularmente interessado nos casos de (1) e (2). Ou seja, casos em que os computadores ajudaram a moldar a intuição humana de maneiras cruciais.
Moritz
2
Algumas das respostas mais recentes a essa pergunta, no final da lista, são excelentes e merecem ser lidas. Sugiro ler até o fim!
András Salamon

Respostas:

32

Um exemplo muito conhecido é o Teorema das Quatro Cores , originalmente comprovado por uma verificação exaustiva.

Evgenij Thorstensen
fonte
6
(Indiscutivelmente) não ciência da computação teórica.
Jeffε
20

Corrija pontos no plano. Seja T uma triangulação (isto é, um gráfico linear plano com os pontos como vértices totalmente triangulados) e permita que o peso da triangulação seja a soma dos comprimentos das arestas.n

Mostrar que o problema da triangulação de peso mínimo (MWT) era NP-difícil era um problema aberto de longa data, dificultado pelo fato de os comprimentos das bordas envolverem raízes quadradas, e a precisão desejada necessária para calculá-las com precisão era difícil de encadernar.

Mulzer e Rote mostraram que o MWT era difícil para o NP e , no processo, usaram a assistência do computador para verificar a correção de seus aparelhos. Até onde eu sei, não há provas alternativas.

Suresh Venkat
fonte
20

A prova de Thomas Hales (seu site, MathSciNet ) da conjectura de Kepler envolveu tanta análise de casos - e os casos foram verificados por computador - que ele decidiu tentar uma prova formal. Seu projeto para fazê-lo é o FlysPecK , e ele estima que serão necessários 20 anos de trabalho.

Pesquisadores em linguagens de programação usam regularmente provas auxiliadas por computador em seus trabalhos, embora eu não saiba o quanto isso é essencial em termos de seu processo de pesquisa (embora isso certamente os impeça de ter que escrever toneladas de manipulações tediosas, no entanto).

Joshua Grochow
fonte
20

Doron Zeilberger fez alguns trabalhos no campo das provas geradas por computador. Mais notavelmente, ele preparou um programa Maple para provar identidades geométricas e outro programa para provar uma classe de identidades combinatórias . Alguns dos métodos são mencionados no livro A = B .

Tomer Vromen
fonte
20

Os computadores também foram usados ​​para determinar os limites superiores nos tempos de execução dos programas de retorno, resolvendo problemas difíceis de NP, e construir dispositivos para provar resultados de inadequação. Este e outros tópicos divertidos esperam por você em um pequeno ensaio (aviso, autopromoção extrema à frente) intitulado "Aplicando a prática à teoria". Veja http://arxiv.org/abs/0811.1305

Dada essa lista legal, parece que eu deveria atualizar o artigo!

Ryan Williams
fonte
Sim, eu também gosto.
Daniel Apon
18

Um contra-exemplo à conjectura de Hirsch , importante para programação linear e combinatória poliédrica, foi proposto por Francisco Santos muito recentemente. A verificação por computador foi usada primeiro para estabelecer algumas das propriedades exigidas no exemplo, embora argumentos sem a ajuda do poder computacional tenham sido descobertos posteriormente, cf. Postagem no blog de Gil Kalai ou artigo sobre arxiv .

RJK
fonte
15

Não vi isso mencionado aqui, mas um provador de teoremas automatizado resolveu o antigo problema aberto de saber se as álgebras de Robbins são booleanas:

http://www.cs.unm.edu/~mccune/papers/robbins/

Isso é especialmente notável porque o computador desenvolveu toda a prova e o problema estava aberto há várias décadas.

Não tenho certeza se ele se qualifica como TCS, mas é possível que esteja intimamente relacionado.

Mugizi Rwebangira
fonte
11
Uma resposta mencionando isso foi publicada em meados de agosto, mas a resposta foi excluída pelo proprietário no final de setembro. É um bom exemplo.
András Salamon
14

O algoritmo Karloff – Zwick para MAX-3SAT atinge o desempenho esperado 7/8. No entanto, a análise baseia-se em desigualdades de volume esférico não comprovadas. Essas desigualdades foram finalmente confirmadas por meio de provas assistidas por computador em outro artigo de Zwick .

Além da prova de Hales à conjectura de Kepler, como mencionado acima, a prova da conjectura do favo de mel e a da conjectura Dodecaédrica também são auxiliadas por computador.

Zeyu
fonte
11
Enquanto estamos nesse sentido, a reprovação de Weaire e Phelan da conjectura Kelvin também foi auxiliada por computador. ( en.wikipedia.org/wiki/Weaire%E2%80%93Phelan_structure )
Peter Shor
11

Você pode conferir a página inicial de Shalosh B. Ekhad . Este computador publica artigos há algum tempo (geralmente com co-autores).

Lev Reyzin
fonte
11

Christian Urban usou o assistente de prova de Isabelle para verificar se um dos principais teoremas de sua tese de doutorado era realmente um teorema [1]. Usando o assistente, algumas alterações precisavam ser feitas, mas o resultado praticamente se manteve.

Da mesma forma, Urban e Narboux também descobriram erros em uma prova em papel e caneta da prova de completude de Crary para verificação de equivalência.

Meikle e Fleuriot formalizaram o Grundlagen de Hilbert em Isabelle e demonstraram que, ao contrário das afirmações de Hilbert, ele ainda contava com sua intuição de formalizar a geometria de uma maneira axiomática (IIRC, havia provas em sua prova derivadas de Hilbert assumindo coisas sobre diagramas) [3] .

[1]: Revisitando a eliminação de cortes: uma prova difícil é realmente uma prova

[2]: Formalizando na prova de completude nominal de Isabelle Crary para verificação de equivalência

[3]: Formalizando Grundlagen de Hilbert em Isabelle / Isar

Dominic Mulligan
fonte
10

Os resultados em " A geometria das árvores de pesquisa binária ", de Demaine, Harmon, Iacono, Kane e Patraşcu, foram desenvolvidos com a ajuda de um software para testar vários esquemas de carregamento e construir bundas ideais para pequenas seqüências de acesso. (E sim, "bundas" é o termo correto.)

Jeffε
fonte
11
Por "bundas", presumo que você queira dizer "Conjuntos Arborally Satisfeitos"? Talvez eu tenha desistido da diversão da sigla. :)
Andrew W.
10

N. Shankar verificou (totalmente e mecanicamente) a prova de Godel do teorema da incompletude e o teorema de Church-Rosser usando o provador do teorema de Boyer-Moore. Há um livro descrevendo como foi feito.

Radu GRIGore
fonte
6

Existem inúmeros exemplos na análise de caso médio de algoritmos. Talvez algumas das primeiras sejam as experiências com computadores que levaram ao artigo "Alguns resultados inesperados de comportamento esperado para embalagem de lixo" de Bentley, Johnson, Leighton, McGeoch e McGeoch em STOC 1984.

Peter Shor
fonte