Le logiciel D∃∀DUCTION propose une aide à l’apprentissage de la démonstration mathématique. Il vise les étudiants en début de licence, mais peut vous être utile jusqu’en L3 si vous ne maitrisez pas les bases de l’écriture d’une démonstration.

Il se présente sous la forme d’une interface graphique, et vous permet de construire votre démonstration pas à pas en visualisant successivement chaque étape de la preuve. Il ne propose pas une rédaction de la preuve : cette partie reste volontairement à la charge de l’étudiant, qui peut s’aider d’une visualisation symbolique de la preuve.

Pour le moment la bibliothèque d’exercices traite essentiellement de théorie des ensembles. Les epsilons arrivent…

Sous le capot, D∃∀DUCTION est développé en Python avec PyQt, et s’appuie sur l’assistant de preuve L∃∀N 3. Je cherche de l’aide : si vous voulez participer, contactez-moi !

Voici une vidéo de démonstration, sur un exercice très simple.

Ce qui est le plus génial, c’est la mémoire de travail qu’il prend en charge (…).
Maintenant je suis persuadée que je pourrai me passer de D∃∀DUCTION !

Une étudiante (particulièrement enthousiaste…)

---

Télécharger D∃∀DUCTION

D∃∀DUCTION est disponible à l’installation sous forme « empaquetée ». Au premier lancement, le logiciel télécharge les dépendances Lean, puis « compile » les énoncés, ce qui peut prendre un peu de temps.

• La version Mac devrait fonctionner sous macOS 10.12 ou ultérieure. Le système bloque l’exécution au premier lancement : ouvrir les préférences système -> Sécurité -> Ouvrir.
• La version Windows devrait fonctionner sous Windows 10 ou ultérieure.
• La version Linux sous Ubuntu 20.04.4 ou ultérieure, et peut-être sous d’autres Linux ? Il faut autoriser l’exécution avant le premier lancement (clic droit -> permissions -> autoriser l’exécution).

Malheureusement, l’installation est assez aléatoire. D∃∀DUCTION sera bientôt disponible dans une machine virtuelle qui devrait fonctionner sans problème sur toute sles plate-forme. Son gros inconvénient est d’occuper une grosse place mémoire.

L’installation est également possible (mais plus délicate) à partir des sources Python.

• Problème sous Mac (sauf avec la machine virtuelle) : Lean nécessite l’application gmp, qui semble ne pas être installée de façon standard sur les Mac. Son absence se traduit par un plantage après le choix de l’exercice (lorsqu’on clique sur « Commencer la preuve »). Dans ce cas, avant de relancer le logiciel, installer gmp en ouvrant un Terminal et en tapant :

brew install gmp

Ceci nécessite Homebrew ; pour l’installer si ce n’est pas déjà fait, taper auparavant :

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

• Cas particulier des nouveaux Mac M1 : l’installation est possible mais particulièrement compliquée sur les nouveaux Mac M1, que ce soit sous forme empaquetée ou à partir des sources : Lean 3 utilise la librairie gmp mais ne sait pas la chercher dans le bon répertoire, qui n’est pas le même qu’avec un processeur Intel ; la solution consiste à installer gmp en utilisant l’émulateur Intel Rosetta.