Claude формализовал Великую теорему Ферма в Lean

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

Важно: Claude не открыл новое доказательство. Великая теорема Ферма уже была доказана Эндрю Уайлсом, а сам математический результат давно известен. Новость в другом: модель смогла перевести это доказательство в машинно проверяемую формализацию, что обычно требует сильной математической подготовки, терпения и владения tooling вокруг proof assistants.

Это важно, потому что формальные доказательства дают редкую для AI область с жесткой проверкой: доказательство либо проходит проверку, либо нет. Если модели смогут стабильно помогать с такой работой, математики и технические исследователи получат более быстрый способ проверять аргументы, переносить результаты в формальные библиотеки и снимать часть ручного труда в proof engineering.

Anthropic подает результат как ранний сигнал того, как AI-системы могут помогать исследовательской математике, но пока остается открытым вопрос, насколько хорошо такой навык переносится за пределы одной громкой формализации.