Claude от Anthropic перевел Великую теорему Ферма в машиночитаемый код

Система Claude от Anthropic перевела классическое математическое доказательство Великой теоремы Ферма в машиночитаемый код. Процесс автоформализации превратил логические рассуждения в структуру, которую компьютер может проверить автоматически без участия человека.

Механизм и результат

Для реализации задачи использовался специализированный язык Lean. В отличие от традиционного математического текста, который интерпретируется человеком, формализация требует строгого соблюдения синтаксиса, где каждое утверждение должно быть логически выведено из аксиом.

Эффект ускорения достигнут за счет использования инструмента Prove2Me. Этот софт оптимизирует рабочий процесс AI-агентов, помогая им выбирать наиболее эффективный следующий шаг в многоэтапных вычислениях, что снижает затраты на инференс и сокращает время разработки с нескольких лет до 11 дней.

Ограничения и особенности

Несмотря на скорость, результат имеет ряд технических нюансов:

• Итеративность: успех был достигнут не с первой попытки. Предыдущие неудачные запуски внесли лишь 7% полезного (не шаблонного) кода в финальный вариант.
• Ресурсозатратность: даже с применением AI полная формализация остается трудоемким процессом, требующим непрерывной работы системы в течение 11 суток.
• Роль человека: участие людей ограничивалось высокоуровневым руководством; прямое написание кода не производилось.

Главное отличие текущего состояния от предыдущих попыток формализации заключается в масштабе и автономности: система смогла самостоятельно выстроить многослойную структуру, охватывающую алгебру, геометрию, теорию чисел и гармонический анализ, опираясь исключительно на математические аксиомы.