Mohan Ganesalingam e Timothy Gowers, negli ultimi anni, hanno concentrato la loro attività di ricerca all’Università di Cambridge su un particolare tema: i processi del pensiero umano nella fase di dimostrazione di un teorema. I due hanno dato vita a un ampio progetto per realizzare programmi capaci di risolvere in modo automatico problemi matematici ancora irrisolti, simulando i processi logici alla base del pensiero umano. Il preprint pubblicato su ArXiv (http://arxiv.org/abs/1309.4501) rappresenta un primo piccolo passo del loro progetto di ricerca.

I matematici sono rimasti affascinati dalla domanda “come organizzano il pensiero i ricercatori quando cercano di dimostrare dei difficili teoremi matematici?”. A partire da questo quesito, i due hanno studiato il pensiero umano e i suoi processi focalizzandosi in particolare sui processi logici che vengono usati dai matematici durante la dimostrazione di un teorema, cercando poi di riprodurli più fedelmente possibile durante la scrittura del loro software. Il risultato è stato un programma capace di risolvere, per ora, semplici problemi matematici, producendo dimostrazioni in stile “umano”, ovvero proprio come se fossero state scritte da un matematico in carne ed ossa.
Nel preprint “Un risolutore di problemi pienamente automatico con output in stile umano”, Ganesalingam e Gowers non solo presentano il loro programma informatico, ma mostrano anche alcune delle dimostrazioni che è stato in grado di produrre (http://people.ds.cam.ac.uk/mg262/robotone.pdf).

 a cura di Alice Sepe