Provas encontradas por computador

11

Em 1996, um problema aberto de longa data foi resolvido por um computador; ou seja, que a álgebra de Robbins e a álgebra booleana são iguais. A prova foi encontrada por um provador de teoremas automatizado.

Além disso, a prova conhecida do teorema das quatro cores contém componentes gerados por computador.

O objetivo desta pergunta é listar as provas encontradas (total ou parcialmente) pelo computador (seja a única prova conhecida ou a descoberta pela primeira vez).

MCH
fonte
2
Alguns grupos finitos simples esporádicos (como o grupo Lyons foram primeiro construído utilizando um computador, ou seja, a sua existência foi prova (parcialmente) gerada por computador.
JP
A questão é "Teoria da complexidade exporimental" sendo usada para resolver problemas abertos está relacionada a esta.
precisa saber é o seguinte
IMHO você precisa distinguir com mais cuidado entre "encontrado" e "marcado". A prova de Gonthier et al. Definitivamente não foi encontrada por um computador.
Gallais
1
Nice Pergunta mas infelizmente quase equivalente a onde e como é que os computadores ajudam a revelar-se um thm
vzn

Respostas:

12

Outro exemplo famoso é a prova de Hales da conjectura de Kepler, que possuía um grande componente auxiliado por computador.

Da Wikipedia :

Em agosto de 1998, Hales anunciou que a prova estava completa. Nessa fase, consistia em 250 páginas de anotações e 3 gigabytes de programas de computador, dados e resultados.

Huck Bennett
fonte
10

Essa é mais uma meta-resposta, pois é uma lista de listas.

  1. Os papéis de Doron Zeilberger . Ele é matemático e seu computador está listado no co-autor Shalosh B. Ekhad em todos os trabalhos em que o computador contribuiu para obter os resultados.

  2. Trabalho de Georges Gonthier . Ele projetou uma prova verificada por máquina do teorema das quatro cores e recentemente trabalhou no teorema de Feit-Thompson. Recentemente, ele concluiu a formalização do Teorema da Ordem Estranha.

  3. O Archive of Formal Proofs contém provas verificadas com Isabelle e inclui teoremas de correção de algoritmos, o teorema de Gauss-Jordan, alguma teoria de ordens, teoria de categorias e muitos outros resultados clássicos.

  4. Formalizando 100 teoremas , contém provas verificadas por máquina de alguns teoremas famosos.

Vijay D
fonte
1
Obrigado. Devo esclarecer que minha pergunta não está preocupada com as provas verificadas / validadas pelos computadores após a descoberta, nem os resultados em que um computador desempenhou um papel derivá-los (é claro que todos nós usamos computadores em nossa pesquisa, mas acabamos acabando com uma matemática matemática prova que não podemos dizer que foi "derivada" de um computador). Estou procurando conjecturas cujas provas foram geradas (total ou parcialmente) por um computador.
MCH 14/01