Institut de Mathématiques de Jussieu-Paris Rive Gauche

Frédéric LE ROUX

Je fais partie du projet "Analyse Algébrique", mes thèmes de recherches sont les systèmes dynamiques en dimension deux, les homéomorphismes hamiltoniens, et les propriétés algébriques des groupes de transformations.

SORBONNE UNIVERSITE

Equipe : Analyse Algébrique

D∃∀DUCTION 0.3999

Ubuntu

Mac

Nouveautés : corrections divers bugs, exercices élémentaires d’arithmétique

Instructions d’installation :

Pour une installation légère sous Linux ou Mac, choisir le premier ou deuxième lien.
Pas de version légère pour Windows pour le moment, utiliser la machine virtuelle.
La machine virtuelle prend une place mémoire importante (autour de 30Go), mais permettra une mise à jour facile. Voici les instructions d’installation :
- Installez le logiciel Oracle VirtualBox VM sur votre système https://www.virtualbox.org/wiki/Downloads (si votre système est Linux et que vous ne tenez pas absolument a avoir la derniere version, il suffit de taper: sudo apt-get install virtualbox virtualbox-ext-pack)
- Téléchargez le fichier : Debian-ProofAssistants.ova
- Dans un explorateur de fichiers, faites un clic droit sur le fichier Debian-ProofAssistants.ova précédemment téléchargé et choisissez ‘Ouvrir avec Oracle VM VirtualBox’ Puis Cliquez sur ‘Importer’
- Dans le logiciel ‘Oracle VM VirtualBox’ cliquez sur la machine « Debian-ProofAssistants » (colonne de gauche) puis sur « Démarrer » (grosse flèche verte)
- Le login est ‘appam’ et le mot de passe est ‘anr’
- Double-cliquer sur le script ‘Deaduction.sh’ qui apparait sur le bureau virtuel

D∃∀DUCTION 0.39

Version Linux (Ubuntu)

Nouveautés :

Une « calculatrice logique » permet à l’utilisateurice de rentrer des objets mathématiques (pour appliquer un théorème, fournir un témoin pour démontrer une propriété existentielle, formuler un nouveau but, etc.)
Nouvelle interface de choix des exercices, avec indication des exercices faits, et possibilité de sauvegarder les preuves.
Boutons de calcul (expérimental) : additionner des inégalités, les enchainer, etc. .
Amélioration de l’affichage des maths.
Résolution de problèmes de ralentissement, ajout d’un bouton pour redémarrer le serveur Lean.

Formulaire pour utiliser une propriété de limite présente dans le contexte : "Quel objet joue le rôle de ε ?

Formulaire pour fournir un témoin démontrant une propriété d'existence : "Quel objet joue le rôle de N'' ?"

Formulaire pour appliquer l'inégalité triangulaire.

Calculatrice Logique, pour remplir les formulaires précédents.

Choisir un exercice, avec affichage de l'énoncé de l'exercice et des exercices déjà résolus