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.
EDITAR
Ao pesquisar, encontrei algo semelhante para funções matemáticas . Não encontrei um para provas no NIST
fonte
Respostas:
O sistema Mizar é um enorme repositório de provas matemáticas. Veja a página da wikipedia e o site oficial .
De wikipedia / Mizar_system # Mizar_language :
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.
fonte
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.
fonte
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!
fonte
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.
fonte