¿Existe un repositorio para la jerarquía de pruebas?

15

Soy asistente de pruebas de autoaprendizaje y decidí comenzar con algunas pruebas básicas y progresar. Como las pruebas se basan en otras pruebas y, por lo tanto, forman una jerarquía, ¿existe un depósito de la jerarquía de pruebas?

Sé que puedo elegir un asistente de pruebas en particular y analizar su biblioteca para extraer su jerarquía, sin embargo, si quiero encontrar la siguiente prueba en una cadena para probar, no puedo cuando no está en la biblioteca.

En mi opinión, imagino un gráfico, probablemente un DAG , de todas las pruebas matemáticas conocidas que se pueden expresar usando declaraciones en inglés, no pruebas usando imágenes . Este sería el mapa maestro (un mapa en el sentido de comenzar en un punto y viajar a otro punto a través de puntos intermedios), y para un asistente de prueba particular, uno tendría un subgrafo del mapa maestro. Luego, si uno quisiera crear una prueba usando un asistente de prueba que se encuentra en el maestro y no en el subgrafo, al comparar los dos gráficos se podría tener una idea del trabajo necesario para crear las pruebas que faltan para el asistente de prueba.

Soy consciente de que las pruebas matemáticas no son necesariamente fáciles de usar para un asistente de pruebas, sin embargo, tener una idea general de qué hacer es mucho mejor que ninguna.

Además, al tener el mapa maestro, puedo ver si hay múltiples rutas de un punto a otro y elegir una ruta que sea más adecuada para el asistente de prueba particular.

EDITAR

Al buscar encontré algo similar para las funciones matemáticas . No encontré uno para pruebas en el NIST

Guy Coder
fuente
1
¿Está buscando un repositorio de código (para dichos sistemas de prueba) o un "repositorio" de pruebas generales (escrito en inglés / notación matemática)? Si es esto último, ¿has visto: proofwiki.org/wiki/Main_Page
Nicholas Mancuso
Me sorprendería encontrar un depósito de pruebas estructurado y completo. Aparte de eso, cada libro de matemáticas es uno.
Raphael
1
@NicholasMancuso Parece prometedor. La cláusula "desde" en las definiciones de prueba parece darme lo que necesito. Sé que la lista no es grande ~ 5,000, pero como principiante puede ser suficiente del mapa para comenzar. Responda y le daré un voto positivo.
Guy Coder
1
No estoy seguro de que exista un gráfico de este tipo: hay declaraciones en matemáticas que no necesariamente se derivan directamente de una serie de otras pruebas. Muchos argumentos geométricos entran en esta categoría. Puede ser posible completarlos, pero podría haber puntos en los que nadie se molestó en probar lo "obvio". Si existiera tal gráfico, creo que sería realmente masivo, tanto en tamaño como en profundidad. No puedo imaginar el número de pasos para pasar de ZFC a la fórmula cuadrática, mucho menos el último teorema de Fermat.
SamM

Respuestas:

11

El sistema Mizar es un gran depósito de pruebas matemáticas. Vea la página de wikipedia y el sitio web oficial .

de todas las pruebas matemáticas conocidas que se pueden expresar usando declaraciones en inglés

De wikipedia / Mizar_system # Mizar_language :

La característica distintiva del lenguaje Mizar es su legibilidad.

Las pruebas se escriben como artículos, de los cuales hay más de mil artículos y más de 50,000 teoremas probados. La página de wikipedia menciona algunas ideas interesantes del " manifiesto QED ", y cómo Mizar podría estar en camino de lograr esto.

Ensalada Realz
fuente
Sabía de la biblioteca Mizar pero no sabía sobre el gráfico. Definitivamente echaré un vistazo a esto cuando tenga la oportunidad.
Guy Coder
9

ProofWiki contiene una cantidad decente de pruebas de varias áreas de las matemáticas. De ninguna manera está completo, pero es un buen punto de partida para lo que desea.

Nicholas Mancuso
fuente
8

Metamath tiene una gran selección de pruebas, construidas desde su núcleo en lógica proposicional.

Dicho esto, carece dolorosamente en términos de teoría CS. ¡Siéntase libre de expandirlo!

jmite
fuente
Eché un vistazo rápido, esto parece prometedor.
Guy Coder
4

Vea el archivo TPTP , Miles de problemas para los probadores de teoremas. Es algo estándar en el campo. Estos son más los "nodos" del gráfico del teorema sobre el que está preguntando. Algunos documentos que se refieren al archivo pueden haber explorado los bordes en este gráfico.

Tenga en cuenta que en el campo de la ATM, la prueba de teorema automatizada y la prueba de teorema asistida, las pruebas son simbólicas y no es realmente factible o plausible estudiar "pruebas en inglés" mientras visualiza.

Sin embargo, puede aprender sobre la paradoja de Richard, que comenzó como una formulación de lenguaje y luego se formalizó simbólicamente. Se dice que es la inspiración para los "antimonios" (contradicciones) encontrados en la teoría de conjuntos temprana que históricamente incluso allanó el camino al teorema de incompletitud de Gödel.

vzn
fuente