Axiom 4 ноября объявила о выпуске формализации всего Stacks Project — открытого справочника по основам современной алгебраической геометрии объёмом примерно 7500 страниц. Компания сообщает, что перевод на язык Lean занимает около 16 млн строк кода и представляет собой единую библиотеку с машинной проверкой доказательств. Это независимый проект компании, а не обновление исходного справочника
Практическая задача библиотеки — избавить математиков и системы искусственного интеллекта от повторного построения длинных цепочек вспомогательных результатов. Готовые определения и теоремы можно подключать к новым доказательствам. Постоянные идентификаторы исходного справочника сохранены: в опубликованном интерфейсе текст сопоставлен с формальным кодом, а связи между результатами показаны графом зависимостей
По описанию разработчика, перевод выполняли согласованно работающие ИИ-агенты: они искали готовые конструкции, строили доказательства и обеспечивали совместимость определений между разделами. При этом проверка доказательства и точность перевода исходного утверждения — разные задачи. Для второй компания описывает автоматизированные проверки и выборочный аудит ключевых определений и теорем; независимая оценка полноты и точности в анонсе не представлена
Что именно пришлось исправить в исходной математике? Компания заявляет о десятках утверждений, которым понадобились уточнения, включая недостающие условия и особые случаи, и сообщает о построенных контрпримерах. Проверка этих конкретных исправлений особенно важна: ценность такой библиотеки определяется не только объёмом кода, но и тем, насколько точно её утверждения передают исходный математический смысл
Первоисточник — Axiom
Сообщите редакции. Существенные исправления мы отмечаем в материале