Le calcul formel est un moyen « moderne » de faire des mathématiques. Il permet d’envisager des activités potentiellement plus riches avec des techniques différentes et d’accéder aussi à des résultats généraux. Notre groupe (INRP- IREM) développe le logiciel Casyopée qui utilise le calcul formel, orienté vers l’étude des propriétés des fonctions. Casyopée offre des possibilités de calcul symbolique, d’exploration graphique et numérique, et permet d’introduire des paramètres. Il nous est apparu nécessaire d’introduire dans Casyopée une démarche de preuve s’ajoutant aux possibilités offertes par le calcul symbolique. Un des menus du logiciel s’intitule « justifier » : l’élève choisit dans une liste, des propriétés ou théorèmes, des boites de dialogue le guident dans sa démarche, le logiciel pouvant lui suggérer des outils pour sa justification. L’élève peut aussi émettre des conjectures et les utiliser dans sa démarche de preuve. Des fonctionnalités du logiciel aident aussi l’élève dans la rédaction de ses preuves. Enfin, le paramétrage du logiciel permet d’adapter le logiciel à des profils différents d’élèves. Dans notre atelier nous présenterons Casyopée à travers des activités expérimentées dans des classes de lycée. Les participants pourront les tester et une discussion pourra avoir lieu sur les possibilités du logiciel.