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).
Respostas:
Outro exemplo famoso é a prova de Hales da conjectura de Kepler, que possuía um grande componente auxiliado por computador.
Da Wikipedia :
fonte
Essa é mais uma meta-resposta, pois é uma lista de listas.
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.
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.
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.
Formalizando 100 teoremas , contém provas verificadas por máquina de alguns teoremas famosos.
fonte
Um exemplo é a prova da inexistência de um plano projetivo de ordem 10 .
Consulte A busca de um plano projetivo finito da ordem 10 e A inexistência de planos projetivos finitos da ordem 10 .
fonte