Az automatizalt formalis matematika szerintem egy gyokeres attores elott all, es itt hatalmas atfedes van a formalis ellenorzessel. Ez a ket temakor alapvetoen rokon. Becslesem szerinte 15-20 even belul eljutunk odaig, hogy a matematikus feladata nem az lesz, hogy problemakat oldjon meg, hanem hogy a megfelelo problemakat kerdezze. Ez most tulzasnak tunhet, de en fogadni merek errre.

A Fields-érmes Gowers is ezen a véleményen van. Egyszer alkalmam is volt megkérdezni, hogy ezt komolyan gondolja-e. Mondta viccesen, hogy ha tényleg így lesz, majd mindenki felnéz rá, hogy ezt ő hogy megjósolta. De aztán komolyabban azt mondta, hogy tényleg reális esélyt lát erre. Azt én is el tudom elképzelni, hogy jól leszűkített problémaosztályokban a formális bizonyítások teret tudnak nyerni, de általában túl merésznek (naivnak?) tartom az elképzelést. Olyan ez, mint amikor az 50-es években a számítógépeket gondolkodó gépeknek tartották vagy mint amikor valaki fél attól, hogy az internet öntudatra kel. Szerintem ez megmarad az élők kiváltságának (egyetemben a kreativitással, fantáziával, érzelmekkel).