«Nessuno si sognerebbe di dire che possiamo produrre latte e zucchero simulando al calcolatore le sequenze formali dei processi di lattazione e di fotosintesi... Ma supponiamo ora di simulare al calco- latore un matematico, e con successo: ci lamenteremmo forse perché... tutto o dello che abbiamo ottenuto sono semplici rappresentazioni di dimostrazioni? Le rappresentazioni di dimostrazioni sono dimostrazioni, no?». La scrittura formalizzata della matematica in linguaggI simbolici, imposta dai logici contemporanei come Frege a Peano quale realizzazione del sogno leibniziano, spesso contestata in ambiente matematico, ha trovato nell'elaborazione meccanica dei testi formali e nell'automatizzazione della deduzione logica per mezzo dei calcolatori la sua giustificazione e la sua esaltazione. Per essere digerite o prodotte da un calcolatore, le dimostrazioni devono essere rappresentate in un linguaggio formale; tuttavia, secondo canoni della logica, una dimostrazione è tale solo se è formalizzabile. Allora i calcolatori che dimostrano teoremi partoriscono genuini prodotti della mente umana. Per negare questa prospettiva, si deve contestare che la sostanza della dimostrazione matematica si trovi nel legame logico di una catena deduttiva: la matematica perde privilegio di luogo della razionalità. Ma intanto la dimostrazione automatica celebra, con il teorema dei quattro colori, i suoi primi grandi successi. In questo saggio sono ricostruite e commentate le polemiche che hanno accompagnato l'introduzione della formalizzazione in mate natica e in informatica, da Peano e Poincaré a oggi, e sono discussi i problemi che questo tipo di dimostrazione solleva sulla natura della matematica.