Résumé
Le mathématicien Akshay Venkatesh a récemment écrit un essai sur l’effet possible sur la pratique mathématique des progrès dans le domaine de la preuve automatique de théorèmes, et en particulier sur nos jugements de valeur concernant les théorèmes. Je soutiendrai que si les ordinateurs deviendront capables de prouver des théorèmes intéressants, ils devront alors porter des jugements de valeur pour eux-mêmes, et que ces jugements refléteront des propriétés objectives du vaste réseau d’énoncés mathématiques bien formés, tout comme les nôtres.
