Прототип Claude за 11 дней создал машинно-проверяемое доказательство великой теоремы Ферма — 13 миллионов строк кода на языке Lean. По оценкам математиков, такая работа обычно занимает около десяти лет.Автор Hi-Tech Mail
Компания Anthropic опубликовала результаты эксперимента: внутренний прототип Claude перевел доказательство великой теоремы Ферма на формальный язык Lean за 11 дней. Итог — 13 миллионов строк машинно-проверяемого кода.
Саму теорему — утверждение о том, что уравнение xⁿ + yⁿ = zⁿ не имеет решений в целых числах при n больше двух — доказали еще в 1994 году математики Эндрю Уайлс и Ричард Тейлор, завершив поиск, который велся 350 лет. Claude решал другую задачу — формализацию. Это перевод математического текста на строгий машинный язык: компьютер проверяет каждый шаг без допущений, предварительно получив «объяснения» всех понятий и фактов, на которых строится рассуждение.
С 2024 года этой же работой занимается команда профессора Кевина Баззарда из Имперского колледжа Лондона — они расширяют математическую библиотеку MathLib. По оценке Баззарда, на полную формализацию ушло бы около десяти лет. Прототип Claude справился с этой задачей за 11 дней.
Результат, однако, не лишен ограничений. Переиспользовать полученный код напрямую в других математических работах не получится.
Ранее мы рассказывали о том, как Anthropic начала скрыто маркировать тексты, созданные Claude.