MI Történik?

Különbség van egy olyan AI között, amely gyorsabban old meg ismert problémákat, és egy olyan között, amely valami valóban újat fedez fel. Az első lenyűgöző. A második mindent megváltoztat. Az Axiom AxiomProver-je éppen most lépte át ezt a határvonalat, amikor bebizonyította a Fel-sejtést, egy valódi, megoldatlan matematikai problémát, amely eddig a szakirodalomban várt arra, hogy valaki (vagy valami) megfejtse. Az AxiomProver három bemenetet kapott: egy dokumentumot, amely hétköznapi nyelven magyarázza a problémát, egy egysoros utasítást („Állítsd fel és bizonyítsd be a Fel-sejtést Lean nyelven”), és a használandó bizonyítás-ellenőrző rendszert. Először elolvasta és megértette a feladatot, meghatározva a matematikai objektumokat és a bizonyítandó állítást. Ezután mindent lefordított Lean-re, egy matematikai bizonyító nyelvre, amely úgy működik, mint egy szigorú bíró. Minden egyes logikai lépést alapelvekből kell levezetni, és a számítógép ellenőrzi minden lépés helyességét. Ezután jött a kreatív rész: az AxiomProver az exponenciális generátorfüggvények módszerét választotta, ami egy olyan technika, ahol a bonyolult diszkrét matematikai mintázatokat simább, folytonos függvényekké alakítják, algebrailag módosítják őket, majd visszakonvertálják az eredeti képlet bizonyításához. Végül az AxiomProver lépésről lépésre végrehajtotta a bizonyítást Lean-ben, ahol minden logikai lépést számítógép ellenőrzött. Az eredmény: egy teljes, formálisan verifikált bizonyítás.