Jordan Ellenberg - Hogy ne tévedjünk - A mindennapi élet rejtett matematikája

A matematikusok majdnem mind elfogadták Hales
bizonyítását, de Hales mintha végig nem tudta volna túltenni
magát azon a rossz érzésen, hogy bizonyítása számítógépre
támaszkodik. A Kepler-sejtés bebizonyítása után elfordult a
geometriától, noha az tette híressé, és áttért a formális
bizonyítások helyességének kutatására. Hales olyan jövendő
matematikát lát maga előtt – és dolgozik is a létrehozásán –,
amely gyökeresen más, mint a mi mostani matematikánk.
Nézetei szerint a matematikai bizonyítások – ha számítógépre
támaszkodnak, ha emberi lény alkotja meg őket papíron,
ceruzával – olyan bonyolulttá váltak és annyira függnek
egymástól, hogy észszerűen már nem lehetünk biztosak a
helyességükben. A véges egyszerű csoportok elmélete, egy már
beteljesült program – annak volt nagyon fontos alkotórésze a
Leech-rács Conway-féle elemzése – szerzők százai által írt cikkek
százaiból állt össze, és ezek a munkák több tízezer oldalt tesznek
ki együttesen. Nincs élő ember, akiről el lehetne mondani, hogy
elejétől a végéig megértette. Hogyan lehetnénk biztosak benne,
hogy csakugyan helyes?
Hales úgy gondolja, hogy nincs más választásunk: újra kell
kezdenünk az egészet, a matematikai tudás hatalmas együttesét
olyan formális szerkezetté kell átalakítani, amely gépileg
ellenőrizhető (és ez, ahogyan Hales meggyőzően állítja, elérhető
cél), mert azután nem kell többé bajlódnunk majd az olyasféle
ellentmondásokkal, amilyet Halesnek kellett elviselnie, hogy egy
bizonyítás csakugyan bizonyítás-e. És mi lesz azután? A
következő lépés talán az lehet, hogy számítógépek