Математичар Кевин Базард са Империјал колеџа у Лондону обучава рачунаре да докажу један од најпознатијих проблема у историји математике: Фермаову последњу теорему.
Решавање тог проблема није поента. Већ постоји прихваћен доказ који је финализован 1998. године. Тај рад је сложени лавиринт математике који обухвата око 130 страница у два рада. Он обухвата више математичких области и уједињује апстрактне идеје које су раније изгледале неповезано.
Познавати тај доказ значи познавати широк део математике. У будућности, каже Базард, рачунарски програм који може да верификује нешто тако обимно моћи ће да помогне математичарима да пронађу, анализирају и решавају широк спектар проблема.
Базард и неколицина математичара годинама уназад раде на пројектима попут овог
Годинама Базард и неколицина математичара раде на пројектима попут овог како би формализовали математику. Историјски гледано, формализација је подразумевала изражавање математичких идеја што прецизније, уз уклањање сваке двосмислености. Данас то значи превођење дефиниција и теорема у рачунарски код како би специјализовани програм могао да провери сваки детаљан корак.
Формализација „је нова парадигма… која суштински захтева да онај ко пише доказ буде много ригорознији него иначе“, каже математичарка Емили Риел са Универзитета Џонс Хопкинс. „Рачунар заправо не попуњава детаље.“ Особа која пише доказ мора да их уради сама.
Али формализовање доказа Фермаове последње теореме је само темељ шире визије: изградње дигиталне библиотеке целе математике која ће омогућити рачунарима да постану корисни асистенти математичарима.
Математика између табле и рачунара
Чак и данас, већина математичара пише доказе користећи описе и интуицију, традиционалне алате који су до недавно изгледали недоступни рачунарима. Због тога је формализација дуго била нишна активност јер захтева изражавање математичких идеја као кода.
Сада, експлозија вештачке интелигенције убрзала је напоре, предвођене технолошким компанијама, да се комбинују велики језички модели са доказивачима теорема ради развоја система способних за аутоматску формализацију. У теорији, такви системи би могли да ураде ствари које људи не могу.
То је подељен циљ, који забрињава многе математичаре због тога како би могао да промени истраживање и напредак у математици. Оно што је почело као филозофско питање — која је максимална прецизност математичког доказа — сада је постало егзистенцијално: да ли ће тежња ка прецизности уздрмати целу област?
„Налазимо се на прагу промене“, каже Патрик Шафтo, математичар и информатичар са Рутгерса и DARPA.
„Математика се данас практикује на табли, као пре 100 година. Али мислим да је врло вероватно да ће за пет година сваки млади математичар користити АИ.“
Мој роботски асистент
Идеја коришћења машина за доказе није нова. Већ 1956. године истраживачи RAND корпорације представили су рачунарски програм (назвали су га „логичка теоријска машина“) који је проверавао доказе из Principia Mathematica, чувеног дела Бертранда Расела и Алфреда Норта Вајтхеда.
„Одушевљен сам што Principia Mathematica сада може да се ради машински“, написао је Расел у писму Херберту Сајмону, једном од твораца система. „Жао ми је што Вајтхед и ја нисмо знали за ту могућност, јер смо изгубили 10 година радећи ручно.“
Иако није постала широка пракса, неки математичари су последњих деценија користили интерактивне доказиваче теорема за проверу постојећих доказа. Један од најпознатијих примера је 1998. године, када је математичар Томас Хејлс објавио да је са својим студентом Самјуелом Фергусоном користио рачунар да докаже Кеплерову хипотезу, проблем оптималног паковања сфера који је поставио Јоханес Кеплер у 17. веку.
Отпор и формализација Кеплерове хипотезе
Доказ је наишао на отпор међу математичарима, који су тврдили да због огромних и сложених рачунских провера људи не могу ручно да потврде сваки корак, па самим тим ни да у потпуности верификују исправност доказа.
Због тога је од 2003. до 2014. године Хејлс користио дигиталне асистенте како би формализовао и поново проверио сопствени доказ.
У фебруару, комбиновањем вештачке интелигенције и интерактивног доказивача теорема, украјинска математичарка Марина Виазовска и други завршили су формализацију доказа Кеплерове хипотезе у осам и 24 димензије — дигиталне верзије рада који је Виазовској донео Филдсову медаљу 2022. године.
Базардов пут ка формализацији
Базардов рад са формализацијом почео је 2017. године, када је, како каже, прошао кроз неку врсту „математичке кризе“. Управо је био рецензент једног рада за научни часопис и након дуге преписке са аутором није могао да утврди да ли је аргумент заиста ригорозан.
Та фрустрација га је навела да преиспита стање у математици и оно што би она могла да постане. „Био сам прилично незадовољан стањем ствари“, рекао је током једног предавања. Почео је да се пита: да ли технологија може да уклони неизвесност у верификацији доказа?
Математичари не улазе у ову област зато да би проверавали детаље туђих доказа, већ да би откривали нове ствари. Ако би верификација могла да се препусти машини, зашто то не искористити?
Lean и дигитализација математике
Базард је почео да учи Lean, који је и програмски језик и интерактивни доказивач теорема. Lean се појавио 2013. године, а развио га је Лéo де Мора, компјутерски научник из Microsoft-а, као систем за формалну верификацију математичких аргумената.
Lean је исти систем који је коришћен за формализацију Виазовскових доказа у фебруару.
Како је Базард све више учио, постајао је све узбуђенији. Почео је да формализацију види као дигитализацију математике, што би могло да модернизује начин на који математичари користе рачунаре.
Он то упоређује са дигитализацијом музике. Када су музичке компаније почеле да продају ЦД-ове, испрва је то деловало као начин да се људи натерају да поново купују оно што већ имају. Али касније је омогућило нове начине приступа и дељења музике, што је додатно убрзано стримингом.
„Дигитализација музике је потпуно променила свет музике“, каже Базард. „Ако дигитализујемо математику, можда ће и она бити потпуно промењена.“
Велика мистерија у малој маргини
Према легенди, око 1637. године француски математичар Пјер де Ферма је записао проблем и напомену у примерак књиге Arithmetica, дела грчког математичара Диофанта из трећег века. Проблем се односи на једначину:
an + bn = cn
Ако је n = 2, знамо да постоји бесконачно решења. У том случају једначина постаје Питагорина теорема, где a, b и c представљају странице правоуглих троуглова.
Ферма је тврдио да не постоје цели бројеви a, b и c који могу да задовоље ову једначину ако је n веће од 2. Поред проблема је написао на латинском: „Имам заиста чудесан доказ ове тврдње, али је ова маргина сувише уска да га садржи.“
Векови без доказа
Фермин син је касније пронашао књигу и белешку, али тек после очеве смрти. Теорема је била једноставна за формулисање, али изузетно тешка за доказивање, и Фермин „изгубљени доказ“ је вековима збуњивао математичаре.
Није никада пронађен његов доказ, а многи сумњају да је уопште постојао или да је био нетачан. Неки чак мисле да је цела тврдња била нека врста интелектуалне шале која је трајала вековима.
Ендру Вајлс и решење проблема
Британски математичар Ендру Вајлс коначно је решио проблем крајем 20. века, а касније је сарађивао са Ричардом Тејлором како би доказ финализовали.
Њихов доказ је користио дубоке и веома апстрактне математичке концепте који нису постојали у 17. веку, повезујући области математике које су се раније сматрале неповезаним.
Последице Фермаовог проблема
Кроз векове, проучавање овог једноставног проблема довело је до великих открића у математици, посебно у теорији бројева.
Један од најважнијих доприноса дошао је 1847. године када је немачки математичар Ернст Кумер доказао да теорема важи за одређене просте бројеве. Он је развио идеје које су постале темељ нове области — алгебарске теорије бројева.
Базард и формализација Фермаове теореме
Године 2023. Базард је покренуо пројекат формализације Фермаове последње теореме, делимично због њене важности и величине, а делимично зато што многе његове колеге са Империјал колеџа истражују идеје које се појављују у доказу.
Он је знао да ће то бити огроман и сложен посао, јер је потребно формализовати сваку дефиницију и сваку помоћну теорему која се користи у доказу. Пројекат је, каже, био тежак и пун неуспелих покушаја.
Велики и растући пројекат
Базард не ради сам. У почетку, каже он, око 30 људи је учествовало у пројекту формализације, сви су писали код за Lean и били су познати сарадници. Многи други су се јављали са идејама или покушавали да се укључе, а нешто више од 60 људи је имало своје доприносе који су верификовани и прихваћени.
Ипак, пројекат је прерастао у интердисциплинарну сарадњу на нивоу који Базард није очекивао. Анонимни теоретичари бројева шаљу идеје, каже он. Прошлог августа, био је на музичком фестивалу недељу дана и вратио се са 7.000 непрочитаних порука у вези различитих делова доказа.
У јануару је пројекат достигао једну од првих важних прекретница. „Доказали смо да је одређена ствар коначна“, каже Базард, што је омогућило следећи корак. Међутим, напор који је био потребан за ту прекретницу навео га је да сумња да ће успети да заврше у планираном року од пет година.
Проблем базе знања у математици
Један од највећих изазова је изградња библиотеке математичког знања унутар Lean система. Базард каже да је то уско грло и за примену вештачке интелигенције у математици.
„У овој области АИ за математику постоји велики проблем — недостају нам квалитетни и занимљиви скупови података“, каже он.
У другом пројекту, који финансира Renaissance Philanthropy, Базард и математичар са Рутгерса Алекс Конторович додатно развијају Lean библиотеку и проширују њену примену формализацијом савремених теорема које представљају врхунска достигнућа математике 21. века.
Последице шире од једног пројекта
Проширење математичког знања у дигиталном облику могло би омогућити математичарима да открију грешке у новим доказима или да процене да ли одређене хипотезе уопште могу да стоје.
Рецензенти научних часописа могли би да се више фокусирају на идеје, уместо на проверу техничких детаља доказа.
„То мења правила игре“, каже Риел. „Докази су дуги и сложени, и грешке се лако провуку.“
АИ као алат за проверу доказа
Доказивач теорема који има приступ великој математичкој бази могао би да препозна грешке, халуцинације и нетачности у доказима које генерише АИ.
Базард каже: „Једна халуцинација може да уништи цео математички аргумент, јер је математика таква.“
Због тога технолошке компаније развијају системе који комбинују моделе као што су Google Gemini и ChatGPT са Lean доказивачем.
Растући АИ изазов
До сада је главни проблем великих језичких модела у математици био тачност. Модели попут ChatGPT-а и Claude-а су бољи у математици него што се очекивало, и стално напредују, али и даље праве грешке.
„Ако одете на ChatGPT и тражите да докаже теорему, он ће вам исписати текст“, каже Риел. „Може звучати добро и користити исправне термине, али нема гаранције да је исправно.“
Када се комбинују са доказивачима теорема попут Lean-а, модели постају много поузданији.
АИ на нивоу математичких олимпијада
Прошлог јула, компанија Harmonic представила је систем Aristotle, који користи Lean за проверу и дораду решења. Он је постигао резултат на нивоу златне медаље на Међународној математичкој олимпијади.
На такмичењу у Аустралији 2025. године, више од 600 учесника је решавало изузетно тешке задатке, а само 72 је освојило злато.
Сличне резултате постигли су и системи Google-а и OpenAI-а.
АИ, формализација и нови резултати
Касније су истраживачи са Рутгерса и UCLA радили на формализацији „теореме о простим бројевима“. Напредак је био спор, али је компанија Math, Inc., уз подршку DARPA програма, успела да заврши посао за само три недеље користећи систем Gauss.
Тај систем комбинује Lean и АИ моделе који аутоматски преводе доказе у формални облик који Lean проверава.
Слично томе, истраживачи су користили системе као што су Aristotle и GPT-5.2 да генеришу и формализују доказе проблема које је поставио Пол Ердош.
Сумње и ограничења
Ипак, Базард је и даље скептичан. Каже да тренутно не постоје праве „заштите“ у системима.
Иако Lean може да потврди формалну исправност кода, то не значи да АИ није погрешно протумачио шта се уопште доказује.
„Може се десити да све изгледа исправно, али да заправо није доказано оно што смо мислили“, каже он.
Будућност математике
Неки математичари верују да ће људи увек бити неопходни, али да ће њихова улога бити другачија.
„Део решавања проблема ће практично нестати“, каже Кристијан Сегеди. Улога људи ће бити да усмеравају математику ка занимљивим правцима, док ће АИ обављати технички део.
Он предвиђа да ће АИ ускоро постати супериоран у формализацији доказа и да ће једног дана моћи да ствара доказе од почетка до краја.
Страхови и критике
Други математичари су забринути. Арвинд Асок сматра да АИ поједностављује математику на погрешан начин и да не разуме њену суштину.
Он је чак престао да даје домаће задатке јер студенти превише користе АИ.
Постоји страх да ће нове генерације изгубити способност дубоког размишљања ако се превише ослоне на машине.
Базард, међутим, тврди да циљ није замена математичара, већ помоћ.
„Само желим да учиним живот својих колега лакшим. Не да их заменим. Заправо покушавам да помогнем.“
