Shadowy vision: spanners in the mechanization of mathematics

Depuis le début du dixseptième siècle, il y eut un certain nombre de tentatives pour automatiser les mathématiques. Mais, en fait, aucune de ses tentatives n'a atteint les espoirs des enthousiastes. Avant du mi-vingtième siècle, la tentative la plus réussie fut celle de Charles Babbage, avec sa Machine Analytique. Lorsque Luigi Menabrea eut analysé les étapes successive à franchir pour que la machine remplisse sa tâche, il n'y eut plus de doute que la machine, une fois constuite, pourrait résoudre deux équations linéaires simultanées avec deux inconnues. Tout de même, Lady Lovelace décrivit le calcul des nombres de Bernoulli. On a souvent suggéré que la machine pourrait aussie effectuer des calculs symboliques, mais personne n'a montré comment la machine pourrait les traiter. De ce point de vue la Machine Analytique a eu le même destin que les machines les plus anciennes. Les affirmations sur ses capacités reposaient sur une grand admiration pour son inventeur, sur son besoin de financement et de re-connaissence, sur le fait que les plupart des enthousiastes ignoraient presque tout les problèmes techniques liés à cette entreprise et aussi sur le fait que la machine n'a jamais été construite.