L a cosa che subito mi ha colpito di Silvia De Toffoli è stata il suo “bilinguismo”: la rara capacità di abitare in due culture molto diverse, che le dà l’opportunità di affrontare una disciplina come la filosofia della matematica in maniera unica, senza pregiudizi o luoghi comuni. De Toffoli (1984) è infatti una filosofa e una matematica: ha un dottorato in matematica conseguito alla Technische Universität Berlin e un secondo dottorato in filosofia presso la Stanford University. Oggi è ricercatrice presso la Princeton University. Ho conosciuto De Toffoli attraverso qualche sua apparizione sulle riviste, ho approfondito poi alcuni suoi articoli e sono riuscito a incontrarla di persona durante un workshop al Dipartimento di Matematica dell’Università di Bologna. L’ho intervistata qualche settimana prima che vincesse una fellowship di un milione di dollari alla Wallenberg Academy. “Sono molto emozionata, è davvero un’occasione unica”, mi ha raccontato quando l’ho ricontattata per complimentarmi. “Il progetto si chiama: Humanizing Mathematical Knowledge: Fallibility, Technology, and Know-How. Si tratta di unire l’epistemologia analitica – cioè la teoria della conoscenza – e la filosofia della matematica”. Lo scopo della ricerca sarà quello di produrre un’analisi del sapere in matematica che non sia ridotto a questioni puramente logiche, ma che tenga in considerazione aspetti che hanno a che fare con il modo in cui noi esseri umani ragioniamo. “Insomma, un’analisi propriamente filosofica (e non psicologica o sociologica). Ma non troppo idealizzata. L’idea è di spiegare come l’oggettività matematica possa essere raggiunta da soggetti che, come tutti noi, sono imperfetti, limitati, e commettono errori”. Durante la nostra intervista avevamo avuto modo di parlare dello scisma fra le cosiddette “due culture”, di come paesi diversi si rapportano alla cultura scientifica, del modo in cui matematica, filosofia, letteratura si intrecciano nella sua visione interdisciplinare. Di come la matematica sia un’attività molto umana, fatta di comunità e confronto con gli altri, piena di conflitti, di buchi e di meraviglia. E dei nostri interessi comuni, a partire da Jorge Luis Borges.
Borges è stato il motivo per cui anche io ho fatto matematica. C’è una frase in Metempsicosi della tartaruga, dove afferma che avrebbe voluto scrivere una “biografia dell’infinito”. Dice: “cinque, sette anni di apprendistato metafisico teologico matematico mi metterebbero in grado forse di pianificare decorosamente questo libro”. Con la grande ingenuità e ambizione dei diciottenni, avevo deciso che sarebbe stato un ottimo percorso di studi, pensavo che in nove anni ce l’avrei fatta. Il mio proposito è fallito miseramente poco dopo, ma Borges, Benoît Mandelbrot (il fondatore della geometria frattale) e Kurt Gödel sono stati i motivi per cui volevo studiare matematica. E uno dei primi shock è stato poi rendermi conto che la matematica che fai all’università non c’entra niente con quelle cose lì. Non le tocchi mai. O almeno a me non è mai capitato.
Purtroppo gli insegnamenti non sono sempre “aperti”: a volte ci sono dei corsi che potrebbero essere collegati ma invece se si fanno da un punto di vista molto teorico o tecnico, non si vedono altri collegamenti. Io ho studiato topologia algebrica leggendo i testi originali di Riemann e Poincaré, ma è stato un grande privilegio, perché all’università generalmente non si fa. Ma hai ragione sul fascino della matematica: fra i libri importanti per me, c’è stato anche Biografia dell’infinito di Paolo Zellini. E ovviamente anche Douglas Hofstadter con Gödel, Escher, Bach. Lo vidi tanti anni fa ad un festival della matematica, e mi stupii anche perché parlava un italiano perfetto.
A Roma, nel 2004! C’ero anche io: Hofstadter ha influenzato moltissime giovani menti. C’era anche John Nash in quell’occasione, e c’era Mandelbrot.
Mandelbrot per me è stato un autore davvero importante, dato il mio amore per le visualizzazioni. Lui credeva moltissimo nel potere di “vedere” la matematica.
Al primo anno di università, con un mio collega che adesso è professore, Giovanni Mongardi, abbiamo fatto un piccolo generatore di frattali con il software Mathematica: era lentissimo, funzionava malissimo, ma era una soddisfazione enorme vedere queste creazioni prendere forma. C’è un lato estetico nella matematica innegabile: non solo visuale, intendo, ma filosofico: che cosa vuol dire “bellezza” in matematica? Quando ho scoperto – sempre al primo anno di università – che la sezione aurea si poteva scrivere anche in forma di frazioni continue, la cosa mi ha scioccata, mi ero fatta anche il poster da appendere in camera.
È una cosa innegabilmente bella, di cui non si capisce il perché.
Qual è stato il tuo percorso di formazione?
A me è sempre piaciuta la matematica fin da quando ero piccola, anche grazie a mio papà, che ha sempre amato i giochi matematici e ha anche fondato un’azienda che si occupa di attività legate ai giochi come la creazione di giochi da tavolo e l’organizzazione di eventi ludici. Al liceo scientifico, invece, mi sono innamorata della filosofia. I primi filosofi dell’antica Grecia erano spesso anche matematici, è celebre la frase affissa sopra l’entrata dell’accademia di Platone: Non entri qui chi non conosce la geometria.
Al momento dell’iscrizione all’università sono stata indecisa dunque fra matematica e filosofia: se fossi stata negli Stati Uniti avrei fatto entrambe le cose, dato che si può. In Italia purtroppo si deve scegliere. E quindi dopo un po’ di incertezza ho deciso per matematica prima, perché rompere il ghiaccio è più difficile. Ho coltivato la filosofia con alcune letture da autodidatta, qualche corso facoltativo, come Storia del pensiero scientifico. A Bologna ho fatto un corso su alcune opere filosofiche di Poincaré – La scienza e l’ipotesi, Il metodo della scienza – e mi sono appassionata.
Poincaré è uno dei tuoi riferimenti, lo citi spesso.
È così. Ha scritto delle cose secondo me molto interessanti anche dal punto di vista filosofico, che sono appunto questi libretti a cui lavorava quando era stanco di fare “cose serie”… Anche dal punto di vista matematico è stato il fondatore di quello che è diventato il mio campo, la topologia algebrica, che lui chiamava “Analysis situs”. Ha fatto lavori molto belli anche sulla visualizzazione della matematica.
Dato che mi è sempre piaciuto viaggiare, ho seguito il secondo anno di università in Canada. Là ho fatto matematica in maniera un pò diversa: in Italia è ultra teorica, mentre là anche più pratica, con molti esercizi. Durante la specialistica ho fatto l’erasmus a Parigi, dove ho fatto questo corso di topologia algebrica con il professore Patrick Popescu-Pampu, a cui sicuramente devo molto del mio amore per Poincaré: lui ci faceva studiare sugli articoli originali, in un corso tecnico, a Matematica. È qualcosa che non si fa mai.
In quel momento sono stata indecisa se intraprendere studi più filosofici, tipo filosofia della scienza o logica, ma alla fine ho continuato con un dottorato in topologia algebrica, questa volta alla Berlin Mathematical School. Lì ho studiato teoria dei nodi, e quando il mio livello di tedesco è diventato sufficiente, anche qualche corso filosofico per dottorandi.
In uno di questi, vennero due professori norvegesi Dagfinn Føllesdall e Øystein Linnebo a farci un seminario di una settimana proprio su filosofia della matematica, ed è stata un’epifania. Ho capito che era la mia direzione. Uno dei due professori mi ha consigliato, dopo il dottorato in matematica, di provare a ottenere un nuovo dottorato negli Stati Uniti – dove è pagato, e dove avrei potuto avere una formazione più solida in filosofia, che mi mancava. Sono riuscita a farlo a Stanford. Dopo altri viaggi ed esperienze di studio, lavoro a Princeton.
Hai fatto anche qualcosa su letteratura e matematica?
Non sistematicamente, ma fa parte della mia formazione. Ho amato molto Musil, e il suo Uomo senza qualità, e Simone Weil. Poi c’è Borges, appunto: per fare un altro esempio, in Pierre Menard, l’autore del Don Chisciotte ci sono collegamenti con la matematica dei giochi – all’inizio del racconto Menard è uno che ha inventato una variante degli scacchi. E ovviamente Borges era anche molto affascinato dal tema dell’infinito.
Ma non sono riuscita ad approfondire a livello filosofico neanche il tema della bellezza matematica. Non troppo, almeno, mi piacerebbe dedicarmici più seriamente. Sono già stati fatti un po’ di lavori ma non li trovo esaustivi, quindi mi piacerebbe analizzare meglio la questione.
Immagino sia difficile trovare qualcuno che abbia solide basi sia in matematica che in filosofia, per studiare la questione in maniera “seria”, accademica, sufficientemente competente per entrambe le comunità. Non ce ne sono molte di persone “bilingue” come te. Un filosofo della matematica spesso non sa davvero fare matematica.
Ci sono dei lavori interessanti, ma sono un po’ isolati. C’è chi per esempio ha fatto degli esperimenti con la risonanza magnetica funzionale, guardando che aree del cervello si attivano quando ad alcuni volontari matematici vengono mostrate certe formule o teoremi. Ci sono anche dei lavori empirici, come sondaggi, questionari. Quindi alcuni dati li abbiamo ma ci vuole anche un po’ di interpretazione. Non è che non ci siano studi a riguardo, ma c’è sicuramente molto spazio per dire di più. Siamo solo all’inizio.
C’è un libro che ha recentemente avuto un buon successo fra i lettori italiani: Quando abbiamo smesso di capire il mondo, dello scrittore cileno Benjamin Labatut. È un esperimento interessante di commistione fra narrativa e non fiction. Racconta, romanzandole, diverse storie di scienza tra cui quella di Shinichi Mochizuki, matematico giapponese che dice di aver risolto la congettura abc, considerata uno dei nodi più difficili da sciogliere, in matematica.
Sia le storie di finzione di Labatut che le storie reali sono enormemente affascinanti, e ci pongono vari interrogativi. Uno degli aspetti, per esempio, di cui ancora non mi capacito, è il fatto che in matematica puoi risolvere teoremi molto importanti, ma può non esserci letteralmente che tre-quattro persone al mondo che capiscono la teoria e la dimostrazione. Non credo ci sia una situazione analoga in altre scienze.
È un grande problema, che trovo pericolosissimo. Se hai un risultato importante, e hai solo tre, quattro persone che possono controllare… chi è che controlla veramente? Scholze, un importante matematico tedesco, ha proposto con un suo collaboratore un nuovo framework matematico sui numeri reali. Era una teoria importante e difficile. Nel presentare i risultati, ha continuamente cercato dei feedback da parte dei matematici, che però gli avevano confessato di non aver mai davvero guardato i dettagli della sua dimostrazione… Perché paradossalmente, più un matematico è famoso, meno è probabile che qualcuno gli farà le pulci. È accaduta la stessa cosa con Voevodsky, celebre matematico che ha praticamente scoperto da solo una lacuna in una sua dimostrazione, dieci anni dopo averla pubblicata.
E ha speso gli ultimi anni della sua vita a promuovere l’uso di software chiamati interactive proof assistant, che praticamente permettono di costruire una prova formalizzata, che può essere controllata nei suoi singoli passaggi. Anche Scholze sta andando in questa direzione. A volte però non è un discorso di tecnica, ma di specializzazione: magari la branca della matematica di cui ti occupi non interessa a nessuno. Il caso di Mochizuki è emblematico in questo senso, perché qui si tratta di una persona che ha apparentemente inventato strumenti nuovi per risolvere una congettura famosa, ma non riesce e non vuole spiegarsi con nessun’altro, se non la sua comunità ristretta di matematici giapponesi. Sicuramente anche il suo carattere “chiuso” non aiuta: lo stesso Scholze è andato qualche settimana in Giappone e discutere della sua dimostrazione, cercando di capire tutti i dettagli della dimostrazione, ma si è arrivati ad un punto morto. Secondo Scholze c’era un passaggio che era problematico e necessitava di essere chiarito meglio. Secondo Mochizuki no, ed è rimasto inamovibile. Scholze alla fine è dovuto tornare in Germania e il problema è ancora lì, dopo anni.
Questo è un ostacolo enorme, ci segnala che c’è una comunità matematica disfunzionale: quando c’è un problema, una comunità che funziona ha le risorse e le procedure per risolverlo, in qualche modo. Legato a questo c’è un progetto che sto scrivendo proprio adesso in collaborazione con Claudio Fontanari, che fa geometria algebrica all’Università di Trento. Proprio su un caso di una controversia che è durata decenni in matematica tra Severi ed Enriques, che sono due degli esponenti principali della scuola italiana della geometria algebrica a cavallo tra il Diciannovesimo e il Ventesimo secolo. Anche qui si tratta di un caso di discordia “recalcitrante”, cioè insoluta, che continua nel tempo: il segno che è la comunità stessa ad avere un problema con i suoi processi e procedure.
Stiamo praticamente parlando di sociologia della scienza.
Sì. Cambia anche la percezione “comune” della matematica: la gente pensa che si possa avere opinioni diverse su tutto tranne che in matematica… Ma non è vero.
E le discussioni non sono solo sugli assiomi! La poca letteratura sul disaccordo in matematica infatti è sempre stata concentrata sugli assiomi. Penso per esempio al dibattito su l’intuizionismo di Brouwer, sui metodi costruttivi, sui grandi cardinali, sull’assioma della scelta nella teoria degli insiemi, sul quinto postulato di Euclide…
Invece anche nella vita “pratica” di un matematico si possono trovare delle controversie su alcune inferenze, cioè il processo di affermare “da questo fatto deriva questo altro fatto”. Ci possiamo chiedere se una “inferenza” sia valida o meno: e una comunità matematica “sana” dovrebbe avere procedure e strumenti per rispondere sempre a questa domanda. Non dico che sia una cosa facile, ma, in teoria, a forza di affrontare insieme tutti i dettagli, si dovrebbe riuscire a trovare un accordo.
Nelle tue conferenze ti ho sentita citare spesso varie scuole di pensiero matematico, tra cui l’intuizionismo di Brouwer. Luitzen Brouwer è stato un personaggio interessante: fra i più restrittivi e “conservatori”, se così si può dire, in matematica, ma anche capace di scrivere un trattato mistico-filosofico come Vita, arte, mistica.
Uno come Brouwer, con il suo approccio costruttivista, non credeva che la matematica fosse l’esplorazione di una verità oggettiva, che esiste all’infuori da noi. Pensava potesse esistere solo ciò che si poteva costruire matematicamente: la matematica è un’architettura interna della mente umana, è una costruzione del soggetto. Per questo, filosoficamente, rigettava alcuni risultati o tecniche importanti (per esempio, alcuni teoremi sull’infinito, o la dimostrazione per assurdo): voleva una matematica più “povera” ma secondo lui più solida, più coerente. Non ha attecchito: i matematici hanno preferito mantenere i loro strumenti. Hilbert diceva: “togliere ad un matematico il principio del terzo escluso è come togliere ad un pugile il pugno destro”. Qualcuno ha proseguito nella sua direzione però: ad oggi la logica intuizionista è una delle più importanti logiche non classiche.
Quindi chi ha “vinto”, come scuola filosofica?
Secondo me non ha vinto nessuna delle tre grandi scuole di pensiero che hanno cercato di capire i cosiddetti fondamenti della matematica: oltre al costruittivismo di Brouwer c’è stato il logicismo di Frege e il formalismo di Hilbert. Il logicismo di Frege aveva l’idea di ridurre la matematica (o, più precisamente, l’aritmetica) alla logica. Non c’è mai riuscito. Il programma di Brouwer, come abbiamo visto, ha avuto anch’esso poca fortuna. Nessuno ha accettato di rigettare la logica classica per la logica intuizionistica, c’era troppo da perdere e poco da guadagnare. Anche qui sono rimasti dei gruppi che studiano logica intuizionistica, ma è una cosa di nicchia. Poi c’è il programma di Hilbert – il formalismo – che è stato più o meno distrutto dai risultati di Gödel, il primo e secondo teorema di incompletezza. Perché comunque Gödel ha mostrato dei limiti interni propri dei sistemi formali – con certe caratteristiche, cioè che siano abbastanza forti per esprimere l’aritmetica – e ha dimostrato che il tentativo di Hilbert di dare solide basi alla matematica non funzionava.
Ci sono poche storie scientifiche eccitanti e incredibili come la storia della matematica nei primi decenni del Novecento. Mi ha sempre stupito come, anche a scuola, si studi il Novecento con le sue “crisi” delle forme e le sue rivoluzioni – nell’arte, nella letteratura, nella musica, in fisica – ma si sia sempre tralasciata la matematica. Faccio fatica a decidere se sia più profonda una crisi della nostra visione della realtà come quella portata dalla meccanica quantistica, o una crisi di quello che ritenevamo un universo ordinato e indubitabile, il paradiso del pensiero razionale, come la crisi che abbiamo vissuto in campo matematico, appunto.
È vero, è una storia incredibile, piena di colpi di scena. Solo un fumetto geniale come Logicomix è riuscito un po’ a renderla come si deve. Su Gödel, però, credo sia un po’ “pericolosa” la vulgata che ne è derivata. Il suo comunque è stato un risultato tecnico, dedicato ai sistemi formali. Ci sono anche tante implicazioni filosofiche ma bisogna guardarle con attenzione. A ogni modo per me è molto affascinante lavorare vicino a quello che era il suo ufficio, all’Institute of Advanced Studies di Princeton. Nella biblioteca dell’istituto, nella scheda di lettura sono ancora segnati i nomi di chi aveva prestito in prestito quel determinato libro. Ancora oggi trovo libri con la firma di Gödel.
Nel 1930 Hilbert aveva pronunciato un famoso discorso ad una conferenza di matematici e fisici, in cui disse “Wir müssen wissen, wir werden wissen”, Noi dobbiamo sapere, noi sapremo! Per ironia della sorte Gödel aveva presentato il suo teorema di incompletezza proprio il giorno prima, di fatto rispondendo: no, non sapremo mai. Le parole di Hilbert sono incise anche sulla sua tomba.
Mi rendo conto che stiamo anche noi, senza volere, riproponendo il topos del matematico genio, isolato, a volte pazzo.
E maschio, fra l’altro. In realtà questa è un’idea pericolosa e abbastanza falsa: eccezioni a parte, la matematica è un’attività collaborativa, e molto “femminile”. Poi in passato ovviamente i matematici erano tutti uomini perché le donne non avevano accesso all’educazione. Emmy Noether, Sof’ja Vasil’evna Kovalevskaja sono state eccezioni. Le matematiche, fino alla laurea specialistica, sono tante, poi si fanno più rare. Quando rimani dentro l’accademia hai sempre problemi a crearti una famiglia. Se sei un uomo è più facile; se sei una donna, per avere figli ci vuole tempo ed energia in maniera maggiore rispetto all’uomo. E questo è il “classico” glass ceiling.
Come vedi tu, dall’alto del tuo punto di vista di una persona che da vent’anni studia e cammina avanti e indietro sul confine, la narrazione delle “due culture”, umanistica e scientifica?
È un discorso di metodi e linguaggi spesso molto diversi. Io sono un po’ nostalgica dei “vecchi tempi”, in cui erano ancora possibili personaggi come Poincaré o Federigo Enriques. Matematici che avevano un’educazione classica, con una profonda cultura umanistica e filosofica. L’Italia è stata fortemente influenzata dal pensiero idealista di Croce e Gentile: la scienza e la matematica è stata sempre messa in secondo piano, anche a livello educativo. Proprio tra Croce ed Enriques ci fu una diatriba forte perché Enriques aveva organizzato un congresso internazionale di filosofia, aveva lavorato molto per cercare di unire queste due culture. Purtroppo non ebbe successo e vinse il pensiero crociano. In Francia, per esempio, molto diverso. La matematica – la sua storia, la sua filosofia – sono molto più rispettate a livello culturale. In Italia, le discipline umanistiche sono ritenute superiori. Rispetto alla Francia si avverte moltissimo, anche rispetto alla classe dirigente – in cui da noi per esempio studiare legge è ancora considerato più importante rispetto ad altre discipline. A livello personale, credo che questa linea netta tra discipline scientifiche e umanistiche sia sbagliata, il mio lavoro è proprio andare lì in mezzo e cercare anche punti in comune interessanti, anche fra luoghi apparentemente lontani come letteratura, arte, filosofia e la matematica. È la mia idea di cultura. All’interno dell’accademia spesso si predilige la specializzazione. Per fare un esempio speculare: negli Stati Uniti, fra i filosofi analitici spesso ci sono tanti studiosi molto tecnici che non si interessano minimamente di cultura umanistica. Senza contare che hanno grosse lacune nella conoscenza della cultura europea, come letteratura e filosofia.
Immagino che il contesto accademico non aiuti il sapere non puramente specialistico: sei obbligato a produrre, a pubblicare o perire come si dice in gergo.
Certamente. In Italia soprattutto, dove per ottenere l’abilitazione scientifica devi pubblicare moltissimo. Negli Stati Uniti devi pubblicare molto meno, ma cose di rilievo, importanti. Secondo me è un sistema in questo decisamente migliore, anche se resta problematico e molto stressante.
Durante uno dei tuoi seminari hai parlato dei folk theorems, in matematica. Cosa sono?
I folk theorems sono teoremi che vengono accettati da una particolare comunità (o sottocomunità) matematica, quando in realtà in letteratura non ci sono delle loro dimostrazioni. Sono dati per scontati, e usati magari in altre dimostrazioni. Questo è ovviamente un problema, la nostra è una disciplina scritta, vogliamo che il nostro “archivio” dei teoremi sia completo.
Il problema è che quando qualcuno si mette di impegno e a pazientemente scrivere tutti i dettagli e i passaggi di questi teoremi, il suo paper non viene accettato, perché il risultato è già conosciuto da tutti… Però non è scritto da nessuna parte! Quindi c’è un paradosso. C’è un problema di assegnazione del merito: merito che, come sappiamo, in accademia è moneta corrente per ottenere borse di ricerca, cattedre, ecc.
Prima accennavi all’uso di computer per aiutare i matematici. Può essere davvero questa la giusta via per affrontare alcuni dei problemi di cui soffre la matematica oggi? Quante tecniche di “assistenza software” esistono?
Sono fondamentalmente due. In quella che viene chiamata computer assisted proof, noi chiediamo al computer di fare dei calcoli che usiamo nelle nostre dimostrazioni: nella congettura di Keplero, o nel teorema dei quattro colori, i matematici hanno costruito la struttura delle dimostrazioni e i computer hanno lavorato di forza bruta calcolando dove serviva. E poi c’è l’altra tecnica, quella degli interactive proof assistant a cui accennavo prima. Si tratta di programmi che dovrebbero aiutarci a “formalizzare” la nostra prova.
Cioè a creare una prova formale, verificata dallo stesso computer. Questi programmi sono interattivi perché ci aiutano a dividere la dimostrazione in tante piccole parti, che possiamo formalizzare passo dopo passo. Alla fine quindi ci permettono di ottenere una dimostrazione che è diventata una sorta di codice e che viene automaticamente verificata dal software. Quello che si ottiene è un teorema matematico (un’affermazione con una sua dimostrazione) in un linguaggio informatico, che il computer stesso ti valida. Questo significa praticamente costruire piano piano un archivio di teoremi matematici scritti in codice: più ce ne sono, meglio potranno funzionare questi strumenti in futuro, perché potranno attingere a più risultati.
Quindi tutto sommato forse lo costruiremo davvero quel famoso “edificio della matematica”.
Sì, anche se è un lavoro molto lungo, e vedremo se e quanti matematici useranno questi software. Recentemente ha aperto nuovi orizzonti l’utilizzo di un nuovo sistema chiamato Lean con cui è stato possibile fare matematica anche molto sofisticata, mentre fino a qualche tempo fa era stato usato solo per risultati più semplici.
Ma tutto ciò non risolve il problema alla base: se i matematici stanno litigando su qualcosa, non sarà certo un software a risolvere la questione. Perché dovresti comunque trovare un consenso su come formalizzare le cose per scriverle in codice… Il software, in sè, è un matematico stupido. Ma con una memoria eccezionale.
Ma tutto ciò non risolve il problema alla base: se i matematici stanno litigando su qualcosa, non sarà certo un software a risolvere la questione. Perché dovresti comunque trovare un consenso su come formalizzare le cose per scriverle in codice… Il software, in sè, è un matematico stupido. Ma con una memoria eccezionale.
Come uno studente pazientissimo e che lavora sodo ma a cui devi spiegare ogni passaggio. Non stiamo parlando propriamente di intelligenza artificiale, ma di strumenti che aiutano noi.
Esatto. Ci aiutano a capire, ma anche a verificare. Ci aiutano a capire in modo diverso (perché per formalizzarlo dobbiamo fare uno sforzo di analisi) ma anche poi a verificare tutti i passaggi e tutta la catena delle inferenze. Una formalizzazione del genere non aiuterebbe per niente a capire il “l’idea centrale” di un teorema. Questo perché ci sono varie forme del comprendere la matematica. A volte è un capire più generale e “olistico”, a volte un capire graduale, a volte un capire l’architettura.
