Nel numero 590 di Nature, uscito il 3 febbraio scorso, è apparso l’articolo di Raayoni, G., Gottlieb, S., Manor, Y. et al. Generating conjectures on fundamental constants with the Ramanujan Machine. in cui viene proposto un approccio algoritmico sistematico, chiamato “la macchina Ramanujan”, per scoprire formule matematiche per costanti fondamentali. Ci spiega meglio di cosa si tratta Cosimo Perini Brogi.

<<Sono passati 25 anni da quando il resoconto di una ricerca originale è stato sottoposto ai nostri redattori per la pubblicazione. Un tempo abbastanza lungo perché la questione allora così ampiamente dibattuta possa essere ripresa in considerazione: qual è il ruolo degli scienziati umani in un’epoca nella quale le frontiere della ricerca scientifica si sono spostate oltre la conoscenza umana? >¹

I lettori di fantascienza avranno subito riconosciuto l’incipit del racconto-articolo “L’evoluzione della scienza umana” pubblicato da Ted Chiang per la prima volta sulla rivista Nature, nel 2000. Il report fantascientifico su un mondo dove l’intera ricerca scientifica è condotta dai computer meta-umani mi è tornato in mente dopo aver letto un articolo (questa volta su un risultato scientifico reale) proposto dalla stessa Nature 21 anni dopo la pubblicazione del racconto di Chiang.

L’articolo in questione descrive una macchina che genera formule regolari di costanti matematiche fondamentali. In altri termini: la macchina lavora alla ricerca di frazioni continue che generino una costante irrazionale data in input. Il suo algoritmo base è già disponibile liberamente online, così da poter essere eseguito sul nostro computer personale; inoltre, secondo la pagina web del progetto, si sta anche lavorando per rendere l’interazione più accessibile per chi non ha grande dimestichezza con i linguaggi di programmazione.

Questo sistema di algoritmi ha un nome evocativo: la macchina di Ramanujan (TRM, in breve). Il matematico indiano è stato incredibilmente perspicace nel formulare congetture in teoria dei numeri. Congetture che, per ammissione dello stesso Ramanujan, gli sarebbero state dettate in sogno da una divinità. In una prospettiva positivista e agnostica, si direbbe che TRM sostituisce così l’ispirazione divina con un sistema di algoritmi che, a livello filosofico, ci portano a riflettere sulla natura dell’intuizione in matematica.

Ma più tecnicamente: come funziona la macchina di Ramanujan? L’input è dato da una costante già nota; TRM avvia un sistema di algoritmi di pattern matching che porta all’individuazione di uno spazio di formule regolari congetturali. Inizia a questo punto un algoritmo di ricerca che raffina e riduce tale spazio, fino a che non viene isolata una formula regolare, che deve poi essere verificata analiticamente. E a questo punto, è possibile in molti casi procedere con un lavoro di ingegneria inversa che ci porta ad una vera dimostrazione della congettura.

Perché, in fondo, TRM fa proprio questo: generare congetture matematiche estremamente accurate, ma che necessitano comunque di una verifica mediante una dimostrazione. Anche per questo, il progetto è aperto ad una collaborazione su più fronti: l’implementazione di nuovi algoritmi e di nuove interfacce umano-computer, certo, ma anche la riprova di quanto ipotizzato dalla macchina stessa. Alla fine, c’era da aspettarselo: l’attività del matematico è fatta tanto del momento intuitivo quanto del momento dimostrativo. Se le ricerche sull’intuizione coinvolgono varie forme del sapere, dall’estetica alle neuroscienze, la dimostrazione è oggetto di studio della logica, e della proof theory in particolare.

Sotto la lente della teoria della dimostrazione, vediamo che alla base di TRM ci sono dati e computazioni numeriche, pertanto la macchina è, in definitiva, un calcolatore numerico inverso, e per questo, da sola, non è in grado di fornire dimostrazioni, ma soltanto pure congetture. Sta al matematico umano trasformare la congettura-output in un vero teorema, ed è possibile raggiungere questa meta attraverso due strade differenti. Il matematico, una volta ricevuto il responso dalla macchina di Ramanujan, può spegnere il computer, e procedere alla maniera tradizionale, armato di carta e matita. Oppure, può rimanere alla tastiera, e usare uno dei molti strumenti (dai calcolatori numerici e simbolici, agli assistenti alla dimostrazione) ad oggi disponibili.

In questo loro preprint, Robert Dougherty-Bliss e Doron Zeilberger hanno optato per rimanere alla tastiera: ispirati da TRM, hanno sviluppato dimostrazioni formalizzate al computer di alcune congetture proposte dalla macchina di Ramanujan, e loro generalizzazioni. In tal modo, hanno mostrato che TRM può essere accompagnata da un suo complemento: avendo a disposizione anche un sistema di calcolo simbolico, sono stati in grado di costruire delle formule regolari (ancora sulla base di frazioni continue) assieme alla dimostrazione formale che una data frazione genera davvero una costante matematica, che è in questo caso output (e non input) del loro algoritmo.

Nella Nature News che accompagna il vero e proprio articolo sulla macchina di Ramanujan, Zeilberger enfatizza TRM e il suo risultato come un successo del ragionamento automatico, parlando di un futuro in cui <<gli umani saranno obsoleti, alla fine>>.

Pur condividendo molte delle istanze positiviste nel settore (delineatesi già con i “Principia Mathematica” di Bertrand Russell e Alfred Whitehead nel 1910), chi scrive ritiene che la completa automazione della matematica non sia un risultato così prossimo o scontato. Come ammettono gli stessi Dougherty-Bliss e Zeilberger, la loro macchina ha avuto bisogno dell’intervento umano per riconoscere opportune generalizzazioni, palesi solo per il matematico in carne ed ossa. Questo non esclude, è ovvio, l’avverarsi del pronostico di Zeilberger, ma suggerisce che, almeno per i prossimi anni, la matematica al computer dovrà fare ancora affidamento sugli assistenti alla dimostrazione più spesso che sugli algoritmi di dimostrazione automatica.

Non fraintendete: questo non è un limite intrinseco. Gli attuali macro-settori del ragionamento automatico (dimostrazione interattiva, verifica automatica, e dimostrazione automatica) non solo continuano a prosperare nei campi della certificazione software o dell’automazione dei processi, ma hanno già suggerito nuovi modi di fare matematica, nuovi strumenti per “insegnare” la matematica ai (e con i) computer, nuovi principi logici e formali per rendere rigorosamente chiara l’attività del matematico tradizionale.

Gli obiettivi raggiunti da TRM e dai lavori pionieristici ad essa collegati forniscono un essenziale complemento all’automazione di questa fase analitica del mestiere, quasi un ampliamento prospettico a coprire il momento sintetico, intuitivo, creativo (nell’accezione artistica del termine) del fare matematica. Ma, allo stato attuale, siamo piuttosto nell’epoca dell’interazione fra umani e macchine: i computer non sono ancora cooperatori veri e propri del matematico, ma, come carta e matita, suoi utilissimi strumenti (e questo non è poco, in ogni caso).

Insomma, il futuro raccontato da Chiang, dove ogni scienziato umano è ormai un traduttore/interprete dei risultati ottenuti dai meta-umani, o anche un divulgatore del sapere prodotto dalle macchine, sembra avvicinarsi per la ricerca in matematica, ma non siamo certi a che velocità ciò avvenga. I risultati legati a TRM suggeriscono che qualcosa è all’orizzonte: per adesso, però… non buttiamo via il temperamatite!

Cosimo Perini Brogi

---

1in Ted Chiang, Stories of Your Life and Others,Tor Books, July 2002, pp. 333, traduzione italiana in Ted Chiang, Storie della tua vita, Stampa Alternativa & Graffiti 2008, Traduzione di Giovanni Lussu. Illustrazioni di Alice Tebaldi.