Assistant de preuve pour écrire des mathématiques

Je voudrais écrire des preuves mathématiques en utilisant un assistant de preuve. Tout sera écrit en utilisant une logique de premier ordre (avec égalité) et une déduction naturelle. Le fond est la théorie des ensembles (ZF). Par exemple, comment pourrais-je écrire la preuve suivante?

Axiome: $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$

Théorème: $\forall x\forall y(\forall z(z\notin x)\land\forall z(z\notin y)\rightarrow x=y)$

Autrement dit, l'ensemble vide est unique.

C'est trivial pour moi d'accomplir cela en utilisant du papier et un stylo, mais ce dont j'ai vraiment besoin, c'est d'un logiciel pour m'aider à vérifier l'exactitude des preuves.

Je vous remercie.

Coq et Isabelle peuvent le faire.

[Coq] Voici un article expliquant comment encoder ZFC dans CIC, sur lequel Coq est basé.

Benjamin Werner: Sets in Types, Types in Sets (1997). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

[Isabelle] Il y a une bibliothèque pour ZF.

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html

Déplacé du commentaire à la suggestion de Kaveh

Vous devez d'abord sélectionner un assistant de vérification. Coq est ce que j'utilise, mais il y en a beaucoup d' autres . Coq est basé sur une logique d'ordre supérieur (le soi-disant calcul des constructions inductives). D'autres assistants de preuve sont basés sur une logique de premier ordre, ils peuvent donc être plus adaptés à vos besoins (modulo les commentaires ci-dessus).

Ensuite, vous devez vous engager à apprendre l'assistant de preuve. Le document lié est un tutoriel pour se familiariser avec Coq. Devenir un expert Coq nécessite des années de dévouement et de pratique, mais des théorèmes simples peuvent être prouvés en un après-midi. La clé pour apprendre Coq ou tout autre assistant de preuve est de faire des preuves, telles que celles du document lié. La simple lecture du document n'aidera que très peu, car toute l'expérience d'interaction avec l'assistant de preuve ne peut pas être bien retransmise sur papier.

En quelques jours, vous devriez être capable de coder des théorèmes simples, comme celui ci-dessus, et de les prouver. Ne vous attendez pas à ce que nous le fassions pour vous. Vous n'apprendrez rien de cette façon.

Lorsque vous réussissez à prouver ces théorèmes, n'hésitez pas à poster vos réponses ici et peut-être à laisser quelques commentaires sur vos expériences.

Êtes-vous prêts à relever le défi?

Il existe de nombreux articles en mathématiques écrits à l'aide de l'assistant de preuve Mizar: http://mizar.org/fm/

Dave Clarke suggère Coq, mais vraiment Isabelle semble être une bien meilleure idée, car il a une bibliothèque pour ZF . Isabelle est également très mature et comprend une grande variété de tactiques et d'extensions.

Je n'ai pas personnellement utilisé Mizar, mais cela pourrait aussi être bon.

comment pourrais-je écrire la preuve suivante?

Dans Isabelle / ZF, vous pouvez écrire quelque chose comme ça

theory csthquestion imports Main

begin

theorem empty_unique:
shows "\<forall> x.\<forall>y.(\<forall>z. (z\<notin>x)) \<and> (\<forall>z.(z\<notin>y)) \<longrightarrow> x=y"
    by auto

end

Comme vous pouvez le constater, Isabelle le prouve automatiquement. Bien sûr, vous pouvez rédiger une preuve plus détaillée si vous le souhaitez vraiment.

Ce même théorème est un exemple travaillé (voir l'exemple 11) dans le tutoriel inclus avec mon logiciel DC Proof 2.0. Téléchargez-le gratuitement sur mon site http://www.dcproof.com