На тајном састанку 2025. године, неки од водећих светских математичара окупили су се да тестирају најновији велики језички модел ОпенАИ, о4-мини.
Стручњаци на састанку били су задивљени колико су одговори модела звучали као прави математичар када је дао сложен доказ.
Оно је признао да модел можда даје убедљиве – али потенцијално нетачне – одговоре.
„Нажалост, вештачка интелигенција много боље звучи као да има тачан одговор него да га заправо добије… тачан или погрешан; увек ће изгледати убедљиво“,
Терри Тао, математичар УЦЛА
„Да сте ужасан математичар, били бисте и ужасан математички писац, и наглашавали бисте погрешне ствари“, Терри Таоматематичар са УЦЛА и добитник престижне Филдсове медаље 2006. године, рекао је за Ливе Сциенце. „Али АИ је прекинуо тај сигнал.“
Наравно, математичари почињу да брину да ће им АИ послати убедљиве доказе који заправо садрже недостатке које је људима тешко открити.
Тао је упозорио да би аргументи генерисани вештачком интелигенцијом могли бити погрешно прихваћени јер они погледај ригорозна.
„Нажалост, вештачка интелигенција је много боља у томе да звучи као да има тачан одговор него да га заправо добије… тачан или погрешан; увек ће изгледати убедљиво“, рекао је Тао.
Он је позвао на опрез у прихватању „доказа“ АИ. „Једна ствар коју смо научили коришћењем АИ је да ако им дате циљ, они ће то учинити варати као луд да постигнемо циљ“, рекао је Тао.
Иако може изгледати у великој мери апстрактно питање да ли заиста можемо да „докажемо” високо техничке математичке претпоставке ако не можемо да разумемо доказе, одговори могу имати значајне импликације. На крају крајева, ако не можемо да верујемо доказу, не можемо да развијемо даље математичке алате или технике из те основе.
На пример, један од највећих нерешених проблема у рачунарској математици, назван П против НП, у суштини поставља питање да ли је уопште лако пронаћи проблеме чија се решења лако проверити. Ако то можемо да докажемо, могли бисмо да трансформишемо заказивање и рутирање, поједноставимо ланце снабдевања, убрзамо дизајн чипова, па чак и да убрзамо откривање лекова. Друга страна је то што проверљиви доказ такође може да угрози безбедност већине актуелних криптографских система. Далеко од тога да је тајанствено, у одговорима на ова питања постоји стварна опасност.
Доказ је друштвени конструкт
Нематематичаре би могло шокирати сазнање да су, у одређеној мери, математички докази изведени од људи одувек били друштвени конструкти – о убеђивању других људи у овој области да су аргументи тачни. На крају крајева, математички доказ се често прихвата као истинит када га други математичари анализирају и сматрају тачним. То значи да широко прихваћен доказ не гарантује да је изјава непобитно истинита. Андрев Гранвиллематематичар са Универзитета у Монтреалу, сумња да постоје проблеми чак и са неким од познатијих и испитанијих математичких доказа које је направио човек.
За ту тврдњу постоје неки докази. „Било је неких познатих радова који су погрешни због малих лингвистичких проблема“, рекао је Гранвилле за Ливе Сциенце.
Можда је најпознатији пример Андрев Вилес‘ доказ Фермаове последње теореме. Теорема каже да иако постоје цели бројеви где је један квадрат плус други квадрат једнак трећем квадрату (као 32+42=52), не постоје цели бројеви који чине исто истинитим за коцке, четврте степене или било које друге веће силе.
Вајлс је славно провео седам година радећи у готово потпуној изолацији, а 1993. је представио свој доказ као серију предавања у Кембриџу, уз велику помпу. Када је Вајлс завршио своје последње предавање бесмртном реченицом „Мислим да ћу ту стати“, публика је проломила громогласан аплауз и Шампањац је отпушен како би се прославило достигнуће. Новине широм света објавиле су победу математичара над проблемом старим 350 година.
Током процеса рецензије, међутим, рецензент уочио значајан недостатак у Вилесовом доказу. Провео је још годину дана радећи на проблему и на крају је решио проблем.
Али за кратко време, свет је веровао да је доказ решен, иако, у ствари, није био.
Системи математичке верификације
Да би се спречила ова врста проблема – где је доказ прихваћен, а да заправо није тачан – постоји корак да се докази појачају оним што математичари називају формалним језицима верификације.
Ови компјутерски програми, чији се најпознатији пример зове Леан, захтевају од математичара да своје доказе преведу у веома прецизан формат. Компјутер затим пролази кроз сваки корак, примењујући ригорозну математичку логику да потврди да је аргумент 100% тачан. Ако рачунар наиђе на корак у доказу који му се не свиђа, он га означава и не пушта. Ова кодирана формализација не оставља простора за језичке неспоразуме за које се Гранвил брине да су мучили претходне доказе.
Кевин Буззардматематичар на Империјал колеџу у Лондону, један је од водећих заговорника формалне верификације. „Почео сам да се бавим овим послом јер сам био забринут да су људски докази непотпуни и нетачни и да ми људи лоше документујемо своје аргументе“, рекао је Буззард за Ливе Сциенце.
Поред провере постојећих људских доказа, вештачка интелигенција, која ради у комбинацији са програмима као што је Леан, могла би да промени игру, кажу математичари.
„Ако натерамо АИ излаз да производи ствари на формално верификованом језику, онда ово, у принципу, решава већину проблема,“ АИ долази са убедљивим, али на крају нетачним доказима, рекао је Тао.
„Постоје радови из математике у којима нико не разуме цео рад. Знате, постоји рад са 20 аутора и сваки аутор разуме свој део. Нико не разуме целу ствар. И то је у реду. Само тако то функционише.“
Кевин Буззард, математичар Империал Цоллеге Лондон
Буззард се сложио. „Желели бисте да мислите да можда можемо да натерамо систем да не само напише излаз модела, већ га преведе у Леан, да га покрене кроз Леан“, рекао је он. Замислио је интеракцију између Леана и АИ у којој би Леан указивао на грешке и АИ би покушао да их исправи.
Ако се АИ модели могу учинити да раде са формалним језицима за верификацију, АИ би тада могла да се позабави неким од најтежих проблема у математици проналажењем веза изван опсега људске креативности, рекли су стручњаци за Ливе Сциенце.
„АИ је веома добар у проналажењу веза између области математике за које не бисмо нужно помислили да их повежемо“, Марц Лацкенбиматематичар са Универзитета у Оксфорду, рекао је за Ливе Сциенце.
Доказ који нико не разуме?
Узимајући идеју о формално верификованим АИ доказима до своје логичне крајности, постоји реална будућност у којој ће АИ развити „објективно исправне“ доказе који су толико компликовани да их ниједан човек не може разумети.
Ово је забрињавајуће за математичаре на потпуно другачији начин. Поставља фундаментална питања о сврси бављења математиком као дисциплином. Која је на крају поента доказивања нечега што нико не разуме? А ако то урадимо, може ли се рећи да смо додали стање људског знања?
Наравно, појам доказа толико дугог и компликованог да га нико на Земљи не разуме није нов за математику, рекао је Базар.
„Постоје радови из математике у којима нико не разуме цео рад. Знате, постоји рад са 20 аутора и сваки аутор разуме свој део“, рекао је Буззард за Ливе Сциенце. „Нико не разуме целу ствар. И то је у реду. Само тако то функционише.“
Буззард је такође истакао да докази који се ослањају на компјутере да попуне празнине нису ништа ново. „Имамо компјутерски потпомогнуте доказе деценијама“, рекао је Буззард. На пример, теорема о четири боје каже да ако имате мапу подељену на земље или регионе, никада вам неће требати више од четири различите боје да засенчите мапу тако да суседни региони никада нису исте боје.
Пре скоро 50 година, 1976. године, математичари су проблем разбили на хиљаде малих случајева који се могу проверити и написали компјутерске програме да верификују сваки од њих. Све док су математичари били уверени да нема проблема са кодом који су написали, били су уверени да је доказ тачан. Први компјутерски потпомогнут доказ теореме о четири боје објављен је 1977. Поуздање у доказ градило се постепено током година и појачано до тачке скоро општег прихватања када је 1997. произведен једноставнији, али ипак компјутерски потпомогнут доказ, а формално верификовани машински проверени доказ је објављен у2005.
„Теорема о четири боје је доказана компјутером“, приметио је Базар. „Људи су били веома узнемирени због тога. Али сада је то једноставно прихваћено. То је у уџбеницима.“
Неистражена територија
Али ови примери компјутерски потпомогнутих доказа и математичког тимског рада се осећају фундаментално другачије од АИ који сам предлаже, прилагођава и верификује доказ – доказ, можда, за који се ниједан човек или тим људи никада не би могао надати да ће га разумети.
Без обзира на то да ли математичари то поздрављају, АИ већ преобликује саму природу доказа. Вековима су чин генерисања и верификације доказа били људски подухвати — аргументи створени да убеде друге људске математичаре. Приближавамо се ситуацији у којој машине могу да произведу непропусну логику, верификовану формалним системима, коју чак ни најбољи математичари неће успети да прате.
У том будућем сценарију – ако се то оствари – АИ ће учинити сваки корак, од предлагања, тестирања, до верификације доказа, „и онда сте победили“, рекао је Лакенби. „Нешто сте доказали.“
Међутим, овај приступ поставља дубоко филозофско питање: ако доказ постане нешто што само компјутер може да схвати, да ли математика остаје људски подухват или се развија у нешто сасвим друго? И због тога се човек запита у чему је поента, приметио је Лакенби.
