A Peking University kutatói egy olyan mesterségesintelligencia-rendszert fejlesztettek ki, amely nemcsak bonyolult matematikai problémák megoldására képes, hanem saját eredményeit is ellenőrzi. A rendszer egy, a Dan Anderson által 2014-ben megfogalmazott sejtést oldott meg, mindössze 80 órányi futási idő alatt. A kutatók az eredményeket egy, az arXiv felületén közzétett preprint tanulmányban ismertették, hangsúlyozva, hogy a bizonyítás formalizálása gyakorlatilag emberi beavatkozás nélkül történt.
A rendszer működésének alapja egy Rethlas nevű érvelési modul, amely a Matlas matematikai keresőmotor segítségével vizsgál különböző megoldási stratégiákat. Az így létrejövő lehetséges bizonyításokat egy második komponens, az Archon dolgozza fel, amely a LeanSearch eszközzel alakítja azokat egy interaktív tételbizonyító rendszer, a Lean 4 számára értelmezhető formává. A Lean 4 egyszerre programozási nyelv és bizonyítási környezet, amely egy több százezer matematikai tételt és definíciót tartalmazó közösségi könyvtárra épül. A kutatók szerint a teljes folyamat során nem volt szükség emberi matematikai döntéshozatalra.
A fejlesztés jelentősége abban rejlik, hogy a matematikai kutatás hagyományosan nehezen automatizálható terület volt. Bár az AI gyorsabban végezte el a feladatot, mint bármely ember, a kutatók megjegyezték, hogy egy matematikus iránymutatása bizonyos pontokon tovább gyorsíthatja a folyamatot. A rendszer képes összekapcsolni a természetes nyelvi érvelést a formális gépi ellenőrzéssel, így megbízhatóbb eredményeket ad, mint a pusztán nyelvi modellek. Bár az eredmények még nem estek át szakmai bírálaton, és a megoldott probléma nem tartozik a legnehezebb, például a Riemann-sejtéshez mérhető kihívások közé, a kutatók szerint ez a megközelítés fontos mérföldkő lehet a matematikai kutatás jövőjében.
