Cette séance de cours présente Coq, un système formel de gestion des preuves. La séance de cours couvre les bases de Coq, y compris la définition des propositions, la démonstration des théorèmes, et l'utilisation de tactiques. Il explore également des concepts comme la disjonction, la conjonction et l'étoile à Coq.