Une preuve formelle est une preuve qui peut être lue et vérifiée par un ordinateur, directement à partir des règles fondamentales de la logique et des axiomes fondateurs des mathématiques. Issue des efforts du début du xx^e siècle visant à placer les mathématiques sur des fondations sûres, la technologie qui sous-tend les preuves formelles s'est développée depuis des dizaines d'années et a fait des progrès remarquables ces dernières années. Notamment, un projet dirigé par Georges Gonthier a abouti à une vérification formelle complète du théorème de Feit-Thompson selon lequel tout groupe fini d'ordre impair est résoluble. Cet exposé décrira les principaux développements récents du sujet.