Axiom Math формално провери проекта Stacks с AI агенти

Axiom Math съобщи, че негови AI агенти са формално проверили Stacks Project — голяма отворена справочна библиотека по математика, създадена от Johan de Jong през 2005 г. Тя обхваща алгебра, геометрия и теория на числата и се разширява с приноси на математици. Математикът от Columbia Peter Woit я сравнява по значение с книгите на Bourbaki.

Компанията е преобразувала около 7 654 страници в приблизително 16 милиона реда код на Lean. Програма, наречена proof assistant, проверява кода ред по ред, за да установи дали логическата структура на доказателствата е последователна. При Stacks задачата е била усложнена от взаимните зависимости между определенията и теоремите, които е трябвало да бъдат запазени в целия формализиран материал.

Главният изпълнителен директор Carina Hong заяви, че агентите са работили паралелно в широка йерархия и сами са откривали задачи. Axiom е обучила и собствени модели за математика. Според компанията резултатът дава на изследователите основа за формализиране на алгебричната геометрия, където досега е имало малко Lean материал. Axiom е основана през март 2025 г., а през март е набрала $200 милиона в Series A, воден от Menlo Ventures.