Claude полностью формализовал Великую теорему Ферма — и сделал это автономно всего за 11 дней

Anthropic утверждает, что это первое полное доказательство теоремы, которое целиком проверено компьютером. Доказательство Великой теоремы Ферма было найдено ещё в 1995 году математиком Эндрю Уайлсом, но проверить его на компьютере до сих пор не удавалось до… этого дня.

Десятки агентов Claude переписали доказательство на языке Lean, создав 13 млн строк кода и потратив 6 млрд токенов за 11 дней. Причём люди вмешивались лишь изредка и давали агентам общие указания. Кевин Баззард, который сам с 2024 года руководит многолетней формализацией теоремы Ферма, назвал результат Claude «экстраординарным достижением».

Доказательство уже выложили на GitHub.

Исходный код