Стартап Axiom Math объявил о завершении формальной верификации Stacks Project — масштабного открытого справочника по алгебраической геометрии и смежным дисциплинам. Для проверки логической целостности доказательств компания использовала парк ИИ-агентов, которые перевели содержание проекта в 16 миллионов строк кода на языке Lean. Этот язык позволяет программным средствам (ассистентам доказательств) пошагово проверять корректность математических утверждений. По словам представителей Axiom, формализация таких фундаментальных работ необходима для создания надежной базы, на которую смогут опираться будущие ИИ-системы при написании программного обеспечения и проведении научных исследований. В компании утверждают, что наличие проверенной математической «подложки» поможет избежать генерации некачественного контента («slop») и ошибок в автоматизированных рассуждениях. В марте 2025 года стартап привлек 200 миллионов долларов в рамках раунда серии А.