Les ordinateurs aideront demain (ou peut-être seulement après-demain) les mathématiciens professionnels à écrire des preuves dans un langage normalisé, et dont la correction sera de ce fait garantie. Dans cet exposé, on va expliquer ce que ça peut vouloir dire, montrer ce qui existe déjà, et recenser ce qu'il reste à faire.

L'exposé sera très élémentaire, surtout si, comme il en est question, une fraction non-négligeable de l'assistance est composée de lycéens.