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 contient de la théorie des ensembles, des epsilon/deltas, un peu d’arithmétique. Les fiches d’activités utilisées en L1 à SU sont disponibles ici.

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…)

---

Installer D∃∀DUCTION

D∃∀DUCTION est disponible sous forme de paquet Python. C’est maintenant la méthode recommandée pour l’installation. Avec cette méthode, la mise à jour très facile.

D∃∀DUCTION est aussi disponible à l’installation sous forme « empaquetée » :

• 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).

Dans tous les cas, au premier lancement, le logiciel propose de télécharger les dépendances Lean et Mathlib, puis « compile » les énoncés, ce qui peut prendre un peu de temps.

• 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, quelle que soit ma méthode : 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 à faire toute l’installation en utilisant l’émulateur Intel Rosetta.