Ratkaisiko tietokone matemaattisen Erdőksen ongelman?

Matemaatikot Alexei Lisitsa ja Boris Konev Liverpoolin Yliopistosta törmäsivät ongelmaan, joka matemaatikkojen on ratkaistava nopeasti:

Onko tietokoneen laskema todistus tosi, jos sitä ei pysty tarkistamaan?

Dataa (cc Buster Benson)

Lisitsa ja Konev laittoivat tietokoneen laskemaan Erdőksen poikkeavuus ongelmaa:

missä k, d ja C ovat mitä tahansa kokonaislukuja ja x_i on sarja lukuja, joista jokainen on vain joko +1 ja -1, nk. ±1–sarja. Esimerkiksi x_i = (−1)ⁱ⁺¹.

Tämän lausekkeen todistaminen oikeaksi tai vääräksi on osoittautunut vaikeaksi. Lisitsan ja Konevan ohjeistama tietokone teki työtä käskettyä ja todisti lausekkeen oikeaksi, jos sarja sisältää yli 1161 lukua ja C=2. Onko todistus oikea? Tietokoneen todistus on 13 Gb pitkä, eli jonkin verran pidempi kuin wikipedia, tai reilun 160 000 sivua tekstiä. Tällainen määrä matemaattista todistusta on mahdoton tarkistaa hallitusti ja järjellisesti. Matemaatikkojen onkin siis ratkaistava, voiko tietokoneen tekemiä todistuksia pitää oikeana, jos niitä ei voida tarkistaa.

- janiope


Lähde:
http://phys.org/news/2014-02-math-proof-large-humans.html#nRlv