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.