*
*

Kurt Gödel (1906–1978).

La Machine peut-elle démontrer ? est le titre d’un article du numéro 8 de Tangente, paru voici trente ans. Il montrait sur des exemples élémentaires que, si un raisonnement permettait de réduire une question à l’analyse d’un nombre fini (et restreint) de cas vérifiables par ordinateur, alors la question relevait d’une démonstration par ordinateur. À l’époque, nombre de mathématiciens rejetaient encore ce principe, arguant (en toute rigueur, à juste titre) qu’il faudrait alors démontrer que le système d’exploitation utilisé était lui-même exempt d’erreurs.