Onde e como os computadores ajudaram a provar um teorema?

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").

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

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.

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).

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 .

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!

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 .

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.

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.

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

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

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.)

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.

A fórmula do algoritmo Bailey-Borwein-Plouffe para calcular o enésimo bit de Pi sem calcular nenhum dos bits mais significativos foi descoberta, segundo Simon Plouffe , usando sistemas à prova de computador.

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.