Sažetak: GPT‑5.4 je za oko 80 minuta rešio Erdős #1196, asimptotsku verziju Konjekture o primitivnim skupovima. AI je ostao u aritmetičkoj sferi i iskoristio von Mangoldtovu funkciju da prevaziđe ranije analitičke prepreke. Formalna Lean verifikacija je u toku; uspeh bi učvrstio rezultat kao strogi matematički dokaz i podstakao dalju raspravu o ulozi AI u istraživačkoj matematici.
AI Rešio Erdősov Problem #1196: GPT‑5.4 Dao „Dokaz Iz Knjige“ Za ~80 Minuta
Studious robot on an ocean liner cruising the North Sea. (Photo by: Planet One Images/UCG/Universal Images Group via Getty Images)UCG/Universal Images Group via Getty Images
Model GPT‑5.4 je za otprilike 80 minuta proizveo dokaz za dugo otvoreni problem označen kao Erdős #1196, a matematičar Jared Duker Lichtman ocenio je rezultat kao „dokaz iz Knjige“ — pohvalu kvaliteta i estetike dokaza koju je zamišljao Paul Erdős.
Šta je problem i zašto je važan
Problem Erdős #1196 je asimptotska verzija Konjekture o primitivnim skupovima iz 1966. godine, koju su postavili Paul Erdős, András Sárközy i Endre Szemerédi. Primitivan skup je skup celih brojeva u kome nijedan član ne deli drugi; prosti brojevi su najpoznatiji primer takvog skupa. Konjektura se tiče ponašanja određenog zbira preko primitivnih skupova kada se posmatraju sve veći brojevi.
Lichtmanova pozadina i ljudski napori
Jared Duker Lichtman proveo je četiri godine tokom doktorskih studija dokazujući da su prosti brojevi "maksimalni" u određenom smislu za primitivne skupove, a zatim je još sedam godina tragao za sledećim pitanjem u toj familiji problema. On i saradnici Gorodetsky i Wong ostvarili su značajan delimični napredak, ali puna konjektura je ostala nedostižna — sve do nedavnog AI odgovora.
Kako je GPT‑5.4 rešio problem
Dok su prethodni pristupi pretežno prelazili iz diskretne aritmetike u realnu analizu, GPT‑5.4 je ostao u aritmetičkom okviru i neočekivano primenio von Mangoldtovu funkciju. Ključni identitet koji je AI iskoristio glasi: zbir von Mangoldtovih težina preko delilaca broja n jednak je logaritmu n, što je usko povezano s jedinstvenom faktorizacijom na proste. Ta ideja je omogućila prevazilaženje tehničkih analitičkih poteškoća koje su ranije blokirale potpuni dokaz.
«Najbliža analogija bi bila da su glavna otvaranja u šahu bila detaljno proučavana, ali AI otkriva novu varijantu otvaranja koju su ljudi prevideli zbog estetskih i konvencionalnih razloga.» — Jared Duker Lichtman
Verifikacija i posledice
Formalna Lean verifikacija AI‑generisanog dokaza je u toku; ukoliko prođe, rezultat će ući u listu matematičkih rezultata koji su strogo provereni i prihvaćeni. Takva formalizacija je ključna da se impresivan izlaz AI‑ja pretvori u „nepromenljive matematičke podatke“ koje mogu koristiti i drugi istraživači.
Šira kontekst i oprez
Ovaj uspeh dolazi u vreme intenzivnog interesovanja za primenu veštačke inteligencije u matematici: DARPA je pokrenula program expMath da ubrza napredak, startup Math Inc. izveštava o formalizacijama složenih dokaza pomoću sistema Gauss, a inicijativa „First Proof“ testira autonomiju AI‑ja na potpuno novim problemima. Istovremeno, matematička zajednica ističe oprez — razlika između zaista nove ideje i kreativne kombinacije postojećih obrazaca iz trening podataka ostaje filozofsko i praktično pitanje.
Bez obzira na diskusije, činjenica da je Lichtman godinama radio na srodnim pitanjima, dok je AI u nešto više od jednog sata pronašao elegantno rešenje koje on opisuje kao „dokaz iz Knjige“, označava važan trenutak u istoriji matematike i alata za otkrivanje novih dokaza.
Izvor: Forbes
Pomozite nam da budemo bolji.
