Az elmúlt hónapokban jelentős fejlődés történt a mesterséges intelligencia által támogatott matematikai bizonyítás terén. A LongCat új fejlesztése, a Flash Prover, egy 560 milliárd paraméterrel rendelkező, nyílt forráskódú modell, amely nem csupán megoldja a matematikai problémákat, hanem képes azokat formálisan is bizonyítani.
Különlegessége, hogy szakterületekre specializált almodellek együttműködése révén működik: egyikük lefordítja a hétköznapi angol nyelvű matematikai feladatokat formális nyelvre, egy másik az összetett tételt kisebb lépésekre bontja, míg egy harmadik az aktuális bizonyítást építi fel, mindezt valós időben és szigorúan ellenőrizve.
A videó kitér a hibadetektáló és önjavító rendszerekre (például a Hiso rendszerre), amelyek kiszűrik a hibás vagy elavult tanítási adatokat, stabilabbá téve ezáltal a tanulási folyamatot. További érdekes kérdésként felmerül, hogy a rendszer hogyan kezeli a formálisan még nem bizonyított sejtéseket, illetve miképp tudja elválasztani azt, ami valóban bizonyítható attól, ami csak feltételezés.
Végül a tesztek kiterjednek a való életből vett alkalmazásokra is, például a banki kamatszámítás témakörére, ahol a modell képes komplex matematikai igazolásokat nyújtani közérthető magyarázattal, hidat képezve az intuíció és a formális matematika között. Kiemelt jelentőséget kap a rendszer ellenőrző mechanizmusa, amely garantálja, hogy egyetlen lépés sem marad ellenőrizetlenül—megnyitva a formális verifikáció új szintjét például a szoftverbiztonság vagy a pénzügyi szerződések terén.
