Existe um repositório para a hierarquia de provas?
Sou assistente de prova de autoaprendizagem e decidi começar com algumas provas básicas e seguir em frente. Como as provas são baseadas em outras provas e, portanto, formam uma hierarquia, existe um repositório da hierarquia de provas?
Eu sei que posso escolher um assistente de prova específico e analisar sua biblioteca para extrair sua hierarquia; no entanto, se eu quiser encontrar a próxima prova em uma cadeia para provar, não posso quando não estiver na biblioteca.
Em minha mente, imagino um gráfico, provavelmente um DAG , de todas as provas matemáticas conhecidas que podem ser expressas usando declarações em inglês, e não provas usando figuras . Esse seria o mapa mestre (um mapa no sentido de começar em um ponto e viajar para outro ponto por meio de pontos intermediários) e, para um assistente de prova específico, haveria um subgráfico do mapa mestre. Então, se alguém quiser criar uma prova usando um assistente de prova encontrado no mestre, e não no subgráfico, comparando os dois gráficos, é possível ter uma idéia do trabalho necessário para criar as provas ausentes para o assistente de prova.
Estou ciente de que as provas matemáticas não são necessariamente facilmente convertíveis para uso com um assistente de provas, no entanto, ter uma idéia geral do que fazer é muito melhor do que nenhuma.
Além disso, ao ter o mapa mestre, posso ver se há vários caminhos de um ponto a outro e escolher um caminho mais adequado para o assistente de prova específica.
Ao pesquisar, encontrei algo semelhante para funções matemáticas . Não encontrei um para provas no NIST
Você está procurando um repositório de código (para os referidos sistemas de prova) ou um "repositório" de provas gerais (escritas em inglês / notação matemática)? Se este último, você já viu: proofwiki.org/wiki/Main_Page
Eu ficaria surpreso ao encontrar um repositório de provas estruturado e abrangente. Fora isso, todo livro de matemática é um.
@NicholasMancuso Parece promissor. A cláusula "from" nas definições de prova parece me fornecer o que eu preciso. Eu sei que a lista não é grande ~ 5.000, mas como iniciante, pode ser suficiente do mapa para eu começar. Faça uma resposta e eu lhe darei uma votação positiva.
Não tenho certeza de que esse gráfico exista - há declarações em matemática que não necessariamente seguem diretamente de uma série de outras provas. Muitos argumentos geométricos se enquadram nessa categoria. Pode ser possível preenchê-los, mas pode haver pontos em que ninguém se preocupe em provar o "óbvio". Se esse gráfico existisse, acho que seria realmente massivo, tanto em tamanho quanto em profundidade. Não consigo imaginar o número de etapas que vão do ZFC à fórmula quadrática, muito menos ao Último Teorema de Fermat.
— SamM 10/10/12
O sistema Mizar é um enorme repositório de provas matemáticas. Veja a página da wikipedia e o site oficial .
de todas as provas matemáticas conhecidas que podem ser expressas usando declarações em inglês
De wikipedia / Mizar_system # Mizar_language :
A característica distintiva da linguagem Mizar é sua legibilidade
As provas são escritas como artigos, dos quais existem mais de mil artigos e mais de 50.000 teoremas comprovados. A página da wikipedia menciona algumas idéias interessantes do " manifesto QED " e como Mizar pode estar a caminho de conseguir isso.
Um enorme gráfico da biblioteca Mizar.
Este documento também pode ser útil: Combinando as ferramentas de apresentação semântica Mizar e TPTP
Eu conhecia a biblioteca Mizar, mas não sabia sobre o gráfico. Desafiadoramente vou dar uma olhada nisso quando tiver uma chance.
O ProofWiki contém uma quantidade razoável de provas de várias áreas da matemática. Não é de forma alguma completo, mas é um bom ponto de partida para o que você deseja.
Metamath tem uma grande variedade de provas, construídas desde o âmago da lógica proposicional.
Dito isto, é dolorosamente inexistente em termos da teoria da CS. Sinta-se livre para expandi-lo!
Dei uma olhada rápida, isso parece promissor.
Veja o arquivo TPTP , Milhares de Problemas para Provedores de Teoremas . É um pouco padrão no campo. Este é mais o "nó" do gráfico do teorema que você está perguntando. Alguns trabalhos referentes ao arquivo podem ter explorado as bordas deste gráfico.
Observe que, no campo do ATM, prova automatizada de teoremas e prova assistida, as provas são simbólicas e não é realmente viável ou plausível estudar "provas no idioma inglês" como você visualiza.
No entanto, você pode aprender sobre o paradoxo de Richard, que começou como uma formulação de linguagem e depois foi formalizado simbolicamente. Diz-se que é a inspiração para "antimonies" (contradições) encontradas na teoria dos conjuntos iniciais que historicamente até abriram o caminho para o teorema da incompletude de Gödel.