Les preuves formelles fournissent une représentation exhaustive et rigoureusement codifiée des énoncés mathématiques et de leurs démonstrations. Les assistants de preuve sont les logiciels qui rendent l'écriture de ces preuves formelles possible en pratique, et ce pour des théorèmes arbitrairement sophistiqués. Ce cours propose une invitation à l'utilisation des assistants de preuve pour les mathématiques, ainsi qu'une introduction à leur fondements, à leur conception et à leur pratique.

Le calcul formel étudie les mathématiques effectives et leur complexité.
Un principe de base est que les équations fournissent souvent de bonnes structures de données pour spécifier leurs solutions. C’est le cas en particulier pour les équations différentielles ou de récurrences linéaires, qui permettent de définir un grand nombre de fonctions classiques en mathématiques ou en physique. Les propriétés des fonctions solutions (ou des suites solutions)sont alors obtenues par des algorithmes qui s’appliquent à ces équations. Cette approche permet de traiter automatiquement des sommes ou intégrales définies, en calculant des équations qu’elles satisfont, grace à une méthode appelée maintenant “création télescopique”.
Le cours effectuera une introduction à ces questions et, si le temps le permet, aux progrès récents réalisés dans le domaine. Au passage, on verra des algorithmes pour calculer rapidement n!, le nombre pi, ou des intégrales de fractions rationnelles.