Un assistant de preuve est un logiciel capable de lire une preuve mathématique, codée sous la forme d'une chaîne d'implications logiques. Si la chaîne est cohérente, le logiciel est satisfait et il certifie l'exactitude de la démonstration; s'il n'est pas satisfait à une certaine maille de la chaîne, il nous empêche d'avancer jusqu'à quand on arrive à le convaincre. Dans cette exposé je montrerai quelques exemples d'un tel dialogue avec un assistant de preuves (en utilisant le logiciel Lean) et je parlerai d'un travail commun avec A. Baanen, S. Daamen et Ashvni N., où on a formalisé une preuve de la finitude du groupe de classes d'idéaux en Lean.