Mākslīgais intelekts Claude atklāj simtiem nezināmu Gēdela pierādītu teorēmu viņa piezīmēs
Somu loģiķis Jans fon Plato ar mākslīgā intelekta modeli Claude dažos dienās izanalizēja austriešu loģiķa Kurta Gēdela 1009 lappušu piezīmju grāmatiņas. Tajās atrasti simtiem līdz šim nezināmu teorēmu, un daļa no tām pārbaudīta ar pierādījumu programmu.
Helsinku Universitātes somu loģiķis Jans fon Plato, izmantojot Anthropic izstrādāto mākslīgā intelekta modeli Claude, ir ātri izanalizējis austriešu loģiķa Kurta Gēdela 16 piezīmju grāmatiņas jeb "darba burtnīcas". Tās rakstītas 20. gadsimta 40. gadu sākumā, un no tām atklājies, ka Gēdels pierādījis simtiem teorēmu, par kurām līdz šim nebija zināms. Atklājums ir būtisks matemātikas vēsturei, jo Gēdela 1931. gada nepilnības teorēmas pārveidoja matemātiku un lika pamatus digitālajam laikmetam.
Grūti lasāms materiāls
Pēc saviem agrīnajiem rezultātiem Gēdels publicēja tikai dažus rakstus, taču nepublicēto manuskriptu apjoms sasniedz desmitiem tūkstošu lappušu. Fon Plato kopš 2017. gada vada projektu, kura mērķis ir izprast burtnīcu saturu: 1009 blīvi rakstītas lappuses par matemātiku un loģiku. Liela daļa teksta ir vācu stenogrāfijā Gabelsbergera sistēmā, kas jau Gēdela laikā bija novecojusi. Projektu atbalsta Eiropas Pētniecības padomes piešķirtais 2,5 miljonu eiro grants. Fon Plato pats apguva šo stenogrāfiju un izveidoja nelielu komandu. Darbs virzījās lēni, aptuveni lappuse nedēļā.
Septembrī, pēc konferences Francijā par mākslīgo intelektu un teorēmu pierādīšanu, viņš Claude parādīja savus transkriptus un sešas savas iepriekš sarakstītās grāmatas par Gēdelu. Pēc dažām dienām tika sagatavots 650 lappušu skaidrojums.
Rezultāti
Fon Plato lūdza modeli atrast visas teorēmas, kurām Gēdelam bija pierādījums, skice vai ideja. Claude atrada 663. Pārbaudot ar pierādījumu verifikācijas programmu Coq, aptuveni 400 apstiprinājās tādā formā, kā uzrakstītas, ap 200 bija jāprecizē, bet aptuveni 50 izrādījās nepareizas. Pēc fon Plato teiktā, burtnīcās ir arī 14 loģikas tēmas, kas nav turpinātas, un vairāki rezultāti, kas citiem pētniekiem kļuva zināmi tikai 70. un 80. gados.
Viens no pirmajiem uzdevumiem bija noskaidrot, vai burtnīcās ir izvēles aksiomas neatkarības pierādījums. 1966. gadā amerikāņu matemātiķis Pols Koens par šādu rezultātu saņēma Fīldsa medaļu, un Gēdels toreiz apgalvoja, ka to bija pierādījis jau 40. gados. Claude atbilde bija, ka gandrīz: Gēdelam trūka viena soļa, jo viena definīcija bija kļūdaina.
Amerikāņu loģiķis Džoels Deivids Hamkinss no Notrdamas Universitātes atzina, ka gadījumā, ja rekonstrukcija izturēs pārbaudi, tā būtu interesanta, taču tas, cik daudz tajā pieder Claude un cik Gēdelam, jānoskaidro vēsturniekiem.
