Che cosa significa essere un genio in matematica? Una volta una mia amica (fisica) mi raccontò di aver avuto questo dialogo con suo fratello (alunno delle elementari):
– Ma tu quanto sei brava in matematica?
– Molto brava.
– Allora dimmi (prende la calcolatrice) quanto fa 30.302.146 per 34.534?
È difficile per chi non la studia direttamente rendersi conto di che cosa vuol dire fare matematica. Certamente, però, non ci si limita a una serie di operazioni meccaniche sempre più complicate: più si sale con il livello e più aumentano, invece, la sottigliezza dei teoremi, l’eleganza delle dimostrazioni, la potenza dei concetti.
Mentre un’operazione come una moltiplicazione a dieci o anche cento cifre è difficilissima per un essere umano, fare il conto è banale per un computer, anzi, è tra le operazioni che considera più elementari. D’altra parte, le situazioni in cui è richiesta astrazione o intuizione o immaginazione offrono a una macchina una sfida tale che è difficile perfino formulare il problema in modo ad essa comprensibile. Questo non afferma la stupidità delle macchine: semmai, è una misura della sofisticazione meravigliosa del cervello umano.
Si può addestrare un computer a lavorare ad alto livello, cioè a fare matematica con dei concetti astratti? Un paio di mesi fa, Timothy Gowers, un celebre matematico britannico, ha chiesto ai lettori del suo blog di valutare in chiarezza e stile dimostrazioni scritte in tre modi diversi, come nell’esempio seguente:
Problem 3. Let
be a complete metric space and let
be a closed subset of
. Then
is complete.
3(a) Consider an arbitrary Cauchy sequence in
. As
is complete,
has a limit in
. Suppose
. Because
is closed,
belongs to
. We’ve proved that every Cauchy sequence in
has a limit point in
. So
is complete.
3(b) Let be a Cauchy sequence in
. Then, since
is complete, we have that
converges. That is, there exists
such that
. Since
is closed in
,
is a sequence in
and
, we have that
. Thus
converges in
and we are done.
3(c) Let be a Cauchy sequence in
. We want to show that
tends to a limit in
. Since
is a subset of
,
is a Cauchy sequence in
. Since
is complete,
, for some
. Since
is a closed subset of
, it must contain all its limit points, so
. So
in
. So
is complete.
Notate innanzitutto che tutte le dimostrazioni sono 1) grammaticalmente corrette 2) matematicamente corrette.
Soltanto due settimane dopo, Gowers ha rivelato che per ogni tripletta di dimostrazioni una era stata scritta da uno studente, una da un dottorando, e una da un programma. E ha chiesto ai suoi lettori di identificare quale delle tre fosse prodotta da una “mente elettronica”. Per quanto circa il 50% dei lettori abbia correttamente identificato il computer, l’altra metà è stata ingannata, con significativa presenza di persone che si dicevano “certe” che la risposta giusta fosse un’altra. Nel suo ultimo post, Gowers rivela nel dettaglio i metodi che ha usato insieme al suo collega Mohan Ganesalingam. È interessante notare che quest’ultimo è in realtà un linguista computazionale e informatico e non un matematico. Di fatto, tutto il loro lavoro si distingue da tentativi precedenti di automated theorem proving per il fatto che si basa unicamente sullo studio di come un matematico ragiona nella sua lingua e non su come dovrebbe ragionare. Invece di ridurre la nostra matematica umana al livello della pura logica, alza il ragionamento logico alle complessità del linguaggio umano facendo lavorare il computer direttamente sull’inglese. Con il vantaggio, tra l’altro, di formulare domande e ottenere risposte nella nostra lingua e non in geroglifici.
Trovo questo risultato bellissimo. Non tanto per la sua utilità per aiutarci a dimostrare teoremi avanzati. Lo vedo piuttosto come un tentativo di far parlare e ragionare un computer come un uomo, che è lo scopo ultimo di quella branca della scienza che si chiama intelligenza artificiale. D’altra parte questo sarebbe un problema molto difficile da aggredire in senso generale: Gowers e Ganesalingam sono partiti dalla matematica perché questo è il campo dove c’è il collegamento più diretto tra come è fatta la lingua e come lavora la logica; come sanno tutti quelli che studiano scienza su libri in inglese, il linguaggio tecnico è facile da capire anche in una lingua straniera.
Mi piace pensare che la matematica sarà il primo campo in cui un uomo e un computer potranno conversare alla pari. Ma anche se questo non succedesse mai, un esperimento del genere ci costringe a pensare a come funziona il nostro “genio”.
PS. Se vi è rimasto il dubbio su quale sia la dimostrazione scritta dal programma, leggetevi il post originale. Anche su questo blog c’è un commento ai risultati di Gowers.