Maurizio Codogno, meglio noto in rete come .mau., racconta come lui vede la matematica, con la scusa di non doverla insegnare né crearne di nuova. David Bessis pensa che si potrebbe sfruttare l’AI per cambiare il modo di pensare la matematica: idee interessanti, ma non so quanto possano essere applicate.

Nel post precedente avevo detto che avrei raccontato in seguito cosa David Bessis pensa della matematica, e ora mantengo la promessa. David Bessis ha scritto Mathematica: Un’avventura alla ricerca di noi stessi (che poi Neri Pozza ha ripubblicato cambiandogli il titolo in “La matematica segreta”, recensito per MaddMaths! da Nicola Ciccoli), uno dei tanti libri che non sono ancora riuscito a leggere. Però ho letto questo suo substack dello scorso aprile, e mi sono fatto un’idea della sua filosofia della matematica.

Il punto di partenza è che secondo Bessis ci sono due versioni della matematica: quella ufficiale e quella segreta. La prima è quella hilbertiana, o se preferite dei Principia Mathematica, che la vede come un sistema di deduzione formale, dove si parte con un certo numero di assiomi e si derivano meccanicamente i teoremi. Un mondo ideale in senso letterale: non ci può essere nulla che sia contemporaneamente vero e falso, le dimostrazioni o sono corrette o non lo sono, e non c’è spazio per cazzate. Prima che mi veniate a rompere le scatole con Gödel, vi faccio notare che non ho scritto da nessuna parte che la matematica sia completa, quindi le ipotesi del teorema di incompletezza non sono soddisfatte. La messa in pratica – si fa per dire – di questa matematica si vede nel fatto che i matematici più considerati sono quelli che hanno dimostrato i teoremi iconici; io aggiungo che anche la matematica studiata a scuola è di questo tipo, anche se le deduzioni formali non sono studiate ma solo fatte imparare a memoria.

Ma poi c’è la seconda matematica, quella segreta: la parte umana della storia. Come dice Bessis, questa è la parte che parla del perché è stata inventata la matematica ufficiale, come possiamo interagire con essa, il suo effetto sui nostri cervelli e le bizzarre tecniche mentali attraverso cui i matematici continuano a espandere il suo territorio. Questa è la matematica intuizionista, al cui club segreto partecipano tutti i matematici: ma la prima regola del Club dell’Intuitività è che non si parla del Club dell’Intuitività, e le altre due sono che se se proprio ne si vuole parlare occorre farlo in maniera diminutiva, come se fosse qualcosa necessario ma puramente accessorio, e la terza è che le definizioni valgono zero punti, il lavoro divulgativo toglie punti, e i posti più importanti vanno appunto a chi ha dimostrato i teoremi più complicati. E questo non lo dice Bessis, ma Godfrey Hardy nel suo famoso Apologia di un matematico: Luisa Saraval traduce così il suo incipit.

Non c’è disprezzo più profondo né, tutto sommato, più giustificato di quello che gli uomini “che fanno” provano verso gli uomini “che spiegano”. Esposizione, critica, valutazione sono attività per cervelli mediocri.

Bessis non è per nulla d’accordo e sintetizza così la sua visione filosofica, che chiama concettualismo: la matematica si appoggia sì su un gioco di simboli formali che non ha significato, ma quando noi ci giochiamo un significato glielo diamo eccome. Il fatto è che questo va contro il codice di onore dei matematici, quello che raccontavo prima sull’importanza delle dimostrazioni e non di quella delle definizioni, e quindi non viene riconosciuto da nessuno.

Ma adesso è arrivata l’IA, e le cose sono completamente cambiate! Penso che tutti siano d’accordo sul fatto che anche quando un LLM (più un proof assistant, più probabilmente un umano che traduce la dimostrazione sensate nel mare di tentativi in un formato aggredibile da Lean per ottenere una formalizzazione) risolve un problema, esso non dà alcun significato a quello che ha trovato, se non quello da anticlimax “questa successione di parole che ho fornito è quella più probabile dato il prompt di input e una piccola percentuale di casualità per non essere proprio del tutto deterministico”. Però a quanto pare le principali aziende legate all’intelligenza artificiale sono convinte che la matematica – quella ufficiale, ovvio – sia “risolvibile”, esattamente come si sono risolti gli scacchi e il go. Sono tutte regole, no?

Certo, i risultati ottenuti dalle IA sono eclatanti, ma secondo Bessis almeno per il momento ci sono almeno tre limiti. Il primo è che le dimostrazioni trovate sono soprattutto tecniche: anche i problemi di Erdős sono fini a sé stessi. Il secondo è più complicato da spiegare e mostra qual è il vero problema dietro tutto questo: l’autoverifica formale fatta da Math, Inc. (il cui motto è per l’appunto “Solve math, solve everything”) della dimostrazione di Maryna Viazovska sull’impacchettamento di sfere in uno spazio a otto dimensioni. Il problema è che mentre le verifiche fatte da Lean usando la libreria Mathlib, creata da umani, sono seguibili passo passo, qui abbiamo 200000 righe di codice assolutamente oscure (Aggiungiamo poi che Math, Inc. ha preso le idee di chi sviluppa Mathlib e poi se l’è gestite per conto suo). Tutto questo può sembrare un semplice caso di lotta per arrivare prima, ma guardatelo dal punto di vista di un matematico. Una dimostrazione (o verifica, in questo caso) comprensibile può far sorgere nuove idee e ampliare la matematica; in questo caso invece abbiamo semplicemente aggiunto una figurina all’album delle dimostrazioni e poi l’abbiamo rimesso via. Il terzo limite è in realtà il punto di forza degli LLM: loro sono bravissimi a trovare corrispondenze tra campi diversi della matematica, che è una di quelle cose che noi eravamo abituati a chiamare “creatività” e “innovazione”. Questo limite insomma diventa nostro più che delle IA, ed è la cosa che ovviamente fa più male.

La conclusione di Bessis è che la comunità matematica dovrebbe ripensare da zero il suo scopo e mettersi a far sì che la gente capisca meglio la matematica e sappia usarla in modo più efficace. Di per sé la cosa non sarebbe impossibile, perché la comunità ha già dimostrato di non essere legata al passato, sia dal punto di vista teorico – pensate a come sono cambiati i fondamenti della matematica tra la fine dell’Ottocento e l’inizio del Novecento – che da quello pratico, con l’adozione di TeX come linguaggio per scrivere matematica. Però il tempo stringe, e cambiare paradigma con il vincolo di fare in fretta e furia non è mai una bella idea.

Che ne penso io? Se mi conoscete, potete immaginare che l’idea di riportare la matematica a qualcosa che possa essere spiegato e non semplicemente inculcato risuona nelle mie corde: non stiamo a discettare su quanto io ci riesca, è sempre difficile passare dalla teoria alla pratica. Ma per quanto io apprezzi lo sforzo di Bessis – anche lui ormai un matematico non praticante, anche se in passato è stato praticante eccome! – di trovare una via di uscita al terremoto IA, ho il sospetto che le cose non andranno così. La mia parte ottimista continua a pensare che almeno allo stato attuale le IA magari innovano trovando nuovi collegamenti che permettono di risolvere problemi, ma non sono in grado di creare nuova matematica né di ampliarla; la mia parte cinica pensa invece che troveremo più che altro matematici più bravi a sfruttare le IA per presentare a nome proprio i risultati che hanno fatto loro trovare; il tutto fino a che non arriverà la singolarità e la professione di ricercatore matematico sarà annientata. Ma tanto al mio livello non mi accorgerò di nulla…

Guarda la pagina di questa rubrica