Problemi a trovare il regalo di Natale giusto? Regalate un teorema!

Sicuramente è un regalo originale e difficilmente si corre il rischio che la persona a cui si regala già lo abbia. E poi riflettiamoci, altro che diamanti, sono i teoremi che restano per sempre!

In fin dei conti, a chi non è mai capitato studiando matematica di immaginare il proprio nome associato ad un teorema, entrando così nella pagine della storia?

Per chi non studia matematica c’è quindi ancora una possibilità per diventare una leggenda, con tanto di certificato che lo attesti. Grazie al sito TheoryMine è possibile avere un proprio teorema senza alcuno sforzo, o meglio pagando solo 15 sterline.

TheoryMine è un software automatico in grado di generare nuovi teoremi per le persone che sperano di raggiungere la fama di Pitagora e di Fermat. “Abbiamo generato nuovi teoremi e i clienti possono dargli il proprio nome, quello di un amico o di una persona cara o il nome che preferiscono.” Ha spiegato Flaminia Cavallo amministratore delegato di TheoryMine, società  che ha sede ad Edimburgo.

Se pensate si tratti di un imbroglio e che alla fine vi ritroverete con una criptica equazione copiata da chissà quale libro, TheoryMine vi tranquillizza sostenendo di avere molta più credibilità rispetto alle compagnie che vendono i nomi delle stelle. “Noi inventiamo teoremi nuovi e la tradizione dice che si ha il diritto di dare nomi a questi teoremi” spiega Alan Bundy, professore di ragionamento automatico all’Università di Edimburgo e altro membro del gruppo TheoryMine. “Ci sono 10 compagnie invece, che vendono stelle e nessuna di loro ha alcuna affiliazione con l’Unione Astronomica Internazionale”.

Effettivamente la dimostrazione automatica dei teoremi è un campo matematico usato dalle case produttrici per garantire che gli algoritmi nel processore funzionino correttamente. Bundy e i suoi colleghi hanno lavorato in questo settore per anni. A  Cavallo è venuta l’idea di TheoryMind durante l’ultimo anno dei sui studi in intelligenza artificiale e matematica all’Università di Edimburgo, avendo scritto per la sua tesi un programma per generare nuovi teoremi.

Il programma funziona in questo modo: dalla sua libreria di conoscenze matematiche  genera un insieme di assiomi e li combina in modo differente, in modo da produrre una serie di congetture.  Usa poi la libreria per scartare quelle che esibiscono controesempi sulla loro veridicità. Vengono anche scartate le congetture troppo complesse. A questo punto il programma applica un ordinamento, noto come “rippling”, che prova varie sequenze di affermazioni logiche fino a che una di queste risulta essere la dimostrazione del teorema.

“E’ un’idea intelligente,” afferma Lawrence Paulson, logico computazionale dell’Università di Cambridge e il creatore di Isabelle, un dimostratore di teoremi che il programma di Cavallo usa. Paulson è più interessato alla teoria che è dietro il nuovo programma, aggiungendo che “parte della tecnologia è piuttosto impressionante e vorrei sperare di trovare altre applicazioni oltre vendere certificati.”

Luca Dixon, un altro membro del gruppo TheoryMine sta studiando la possibilità di usare le stesse tecniche per chiarire le regole dell’algebra nell’informatica quantistica, che utilizza regole matematiche diverse dall’informatica classica.

Se state già pensando al discorso da pronunciare quando riceverete la medaglia Fields, avrete una delusione infatti “Non possiamo dire che non succederà mai, ma i teoremi che vengono generati dal programma non sono il genere di cose che possono cambiare il mondo” ha detto Dixon. Va bene non sarà rivoluzionario, ma per lo meno il vostro teorema sarà unico, il software di TheoryMine infatti ignora varianti banali di teoremi già dimostrati.
 
A voi la scelta, è più gratificante un risultato già pronto ottenuto senza alcuno sforzo o  un teorema ottenuto con il “sudore della fronte”?