Pour qu'un théorème soit juste, il faut qu'il soit démontré. Ce qui nécessite des dizaines et des dizaines de pages de raisonnement... qu'un logiciel, baptisé Coq, permet aujourd'hui de vérifier automatiquement et, surtout, de valider, sans erreur possible. De quoi révolutionner les maths !

Bien qu'ils aident les mathématiciens lors de leur phase expérimentale de recherche, les ordinateurs laissent aussi s'introduire de l'incertitude en mathématiques parce qu'ils conduisent parfois à des résultats invérifiables.