Проект под руководством Кевина Баззарда из Имперского колледжа Лондона изначально планировался как многолетняя инициатива математического сообщества. Claude радикально сократил сроки, действуя автономно: десятки параллельных агентов переводили математические понятия в машинный код и доказывали промежуточные утверждения. В итоге система сгенерировала 29 500 верифицированных теорем, потратив около 6 миллиардов выходных токенов.
Итоговый результат в пять раз превосходит объём основной библиотеки формализованных доказательств Mathlib. Проверка через систему Lean подтвердила: доказательство опирается всего на три стандартные аксиомы и полностью соответствует оригиналу Уайлса. Баззард назвал этот прорыв экстраординарным достижением автоформализации, отметив, что ИИ впервые взял на себя задачу, которая раньше требовала титанических усилий профессиональных математиков.
Значение этого события выходит за рамки конкретной теоремы. Современные математические работы становятся настолько сложными, что их рецензирование людьми растягивается на годы. Автоматическая формализация предлагает решение проблемы ошибок в масштабных логических конструкциях. Теперь ИИ может стать инструментом, который мгновенно проверяет корректность новых открытий, обеспечивая надёжный фундамент для дальнейших исследований.
Комментарии (0)
Пока нет комментариев. Будьте первым!