Axiom Math обяви в сряда, че е завършила формалната проверка на Stacks Project — мащабен математически справочник с отворен код. Според компанията нейните AI агенти са преобразували около 7654 страници в приблизително 16 милиона реда компютърно проверен код на езика Lean.

Stacks Project е започнат през 2005 г. от математика Йохан де Йонг от Колумбийския университет. Оттогава сътрудници го разширяват с определения и резултати в алгебрата, геометрията и теорията на числата — от университетско ниво до напреднали разработки.

При формализацията математическите доказателства се записват като код на Lean, а програма за проверка на доказателства проверява логическите им стъпки. За библиотека като Stacks задачата не се изчерпва с отделните теореми: определенията и резултатите зависят едни от други. Изпълнителният директор на Axiom Карина Хонг обяснява пред TechCrunch, че екипът е трябвало да запази тези връзки и съгласуваността между определенията в целия код.

Екипът е задал на агентите обща йерархична структура, без да определя подробно всяка тяхна задача. По думите на Ашвин Сваминатан от техническия екип агентите сами са откривали задачи, които могат да изпълняват паралелно. Axiom е обучила и собствени модели с математическа насоченост, а в началото експерт по Lean е насочвал работата на агентите.

Според Сваминатан резултатът осигурява основа за нови формализирани доказателства в алгебричната геометрия — област, в която досега е имало голяма празнина. Идеята на Axiom е вече проверените резултати да се използват повторно като градивни елементи, вместо всяко следващо доказателство да започва от нулата.

Компанията цели подобни проверени библиотеки да служат на AI агенти и при изграждането на софтуерна инфраструктура. Според Хонг надеждната, многократно използваема база от знания ще позволява на агентите да надграждат работата си, без да натрупват проблеми от лоши първоначални инженерни решения.