Verifica automatica del ragionamento matematico

Sommario. Controllare la correttezza di un ragionamento matematico, quando questo sia completamente formalizzato, `e un compito che pu`o essere delegato ad una macchina. Nasce in questo modo la Matemati- ca Verificata al Calcolatore, una disciplina prossima alla forse piu` nota Dimostrazione Automatica dei Teoremi, ma da questa distinta per me- todologie e obiettivi. Questo articolo si propone di presentare la verifica automatica delle dimostrazioni e di offrire alcuni spunti di riflessione sulle possibili implicazioni culturali e pratiche che questo nuovo settore di ricerca potrebbe offrire.