Existe-t-il un référentiel pour la hiérarchie des preuves?

15

Je suis des assistants de preuve auto-apprenants et j'ai décidé de commencer sur quelques preuves de base et de progresser. Étant donné que les preuves sont basées sur d'autres preuves et forment donc une hiérarchie, existe-t-il un référentiel de la hiérarchie des preuves?

Je sais que je peux choisir un assistant de preuve particulier et analyser sa bibliothèque pour extraire sa hiérarchie, mais si je veux trouver la prochaine preuve dans une chaîne à prouver, je ne peux pas quand elle n'est pas dans la bibliothèque.

Dans mon esprit, j'imagine un graphique, probablement un DAG , de toutes les preuves mathématiques connues qui peuvent être exprimées en utilisant des énoncés en anglais, pas des preuves en utilisant des images . Ce serait la carte principale (une carte dans le sens de commencer à un point et de voyager vers un autre point via des points intermédiaires), et pour un assistant de preuve particulier, on aurait un sous-graphique de la carte principale. Ensuite, si l'on voulait créer une preuve à l'aide d'un assistant de preuve trouvé sur le maître et non sur le sous-graphique, en comparant les deux graphiques, on pourrait avoir une idée du travail nécessaire pour créer la ou les preuves manquantes pour l'assistant de preuve.

Je suis conscient que les preuves mathématiques ne sont pas nécessairement facilement convertibles pour une utilisation avec un assistant de preuve, mais avoir une idée générale de ce qu'il faut faire est bien mieux que rien du tout.

De plus, en ayant la carte principale, je peux voir s'il y a plusieurs chemins d'un point à un autre et choisir un chemin qui convient mieux à l'assistant de preuve particulier.

ÉDITER

En cherchant, j'ai trouvé quelque chose de similaire pour les fonctions mathématiques . Je n'en ai pas trouvé de preuves au NIST

Guy Coder
la source
1
Recherchez-vous un référentiel de code (pour lesdits systèmes de preuve), ou un "référentiel" de preuves générales (écrit en notation anglaise / mathématique)? Si ce dernier, avez-vous vu: proofwiki.org/wiki/Main_Page
Nicholas Mancuso
Je serais surpris de trouver un référentiel de preuves structuré et complet. En dehors de cela, chaque livre de mathématiques est un.
Raphael
1
@NicholasMancuso semble prometteur. La clause "from" dans les définitions de preuve semble me donner ce dont j'ai besoin. Je sais que la liste n'est pas longue ~ 5 000, mais en tant que débutant, il me suffira peut-être de la carte pour commencer. Faites-en une réponse et je vous donnerai un vote positif.
Guy Coder
1
Je ne suis pas sûr qu'un tel graphique existe - il y a des énoncés en mathématiques qui ne découlent pas nécessairement directement d'une série d'autres preuves. De nombreux arguments géométriques entrent dans cette catégorie. Il peut être possible de les remplir, mais il pourrait y avoir des points où personne n'a pris la peine de prouver «l'évidence». Si un tel graphique existait, je pense qu'il serait vraiment énorme, à la fois en taille et en profondeur. Je ne peux pas imaginer le nombre d'étapes pour passer de ZFC à la formule quadratique, encore moins le dernier théorème de Fermat.
SamM

Réponses:

11

Le système Mizar est un énorme référentiel de preuves mathématiques. Voir la page wikipedia et le site officiel .

de toutes les preuves mathématiques connues qui peuvent être exprimées en utilisant des énoncés en anglais

De wikipedia / Mizar_system # Mizar_language :

La particularité de la langue Mizar est sa lisibilité

Les preuves sont écrites sous forme d'articles, dont il existe plus d'un millier d'articles et plus de 50 000 théorèmes éprouvés. La page wikipedia mentionne quelques idées intéressantes du " manifeste QED ", et comment Mizar pourrait être sur la bonne voie pour y parvenir.

Realz Slaw
la source
Je connaissais la bibliothèque Mizar mais je ne connaissais pas le graphique. J'y reviendrai avec défi lorsque j'en aurai l'occasion.
Guy Coder du
9

ProofWiki contient une quantité décente de preuves provenant de divers domaines des mathématiques. Ce n'est en aucun cas complet, mais c'est un bon point de départ pour ce que vous voulez.

Nicholas Mancuso
la source
8

Metamath dispose d'une large sélection de preuves, construites directement à partir de leur noyau dans une logique propositionnelle.

Cela dit, il manque cruellement en termes de théorie CS. N'hésitez pas à l'agrandir!

jmite
la source
J'ai jeté un coup d'œil, cela semble prometteur.
Guy Coder
4

Voir l' archive TPTP , Des milliers de problèmes pour les fournisseurs de théorèmes. C'est quelque peu standard dans le domaine. Il s'agit plus des "nœuds" du graphe théorème que vous demandez. Certains articles faisant référence à l'archive ont peut-être exploré les bords de ce graphique.

Notez que dans le domaine de l'ATM, de la démonstration automatisée de théorèmes et de la démonstration assistée de théorèmes, les preuves sont symboliques et il n'est pas vraiment possible ou plausible d'étudier les "preuves en langue anglaise" comme vous le visualisez.

Cependant, vous pourriez en apprendre davantage sur le paradoxe de Richard qui a commencé comme une formulation de langage et a ensuite été formalisé symboliquement. On dit qu'il est l'inspiration des «antimonies» (contradictions) trouvées dans la théorie des premiers ensembles qui, historiquement, a même ouvert la voie au théorème d'incomplétude de Gödel.

vzn
la source