Последняя теорема Ферма, формализованная агентами искусственного интеллекта всего за 11... — 5 сентября 2026 г. в 13:08:32.464
Последняя теорема Ферма, формализованная агентами искусственного интеллекта всего за 11 дней 😇 👥 Ожидалось, что преобразование доказательства последней теоремы Ферма в код, который могут проверить компьютеры, займет годы – Клод ИИ из Anthropic справился с этим менее чем за две недели ‼ Компания Anthropic, специализирующаяся на искусственном интеллекте, создала формализованное доказательство Великой теоремы Ферма. Группе ИИ-агентов потребовалось всего 11 дней, чтобы выполнить задачу и подтвердить, что доказательство, предложенное человеком в 1990-х годах, верно. Великая теорема Ферма ставила в тупик математиков на протяжении веков, пока она не была доказана в 1995 году Эндрю Уайлсом. В ней утверждается, что не существует целых чисел a, b и c, удовлетворяющих уравнению aⁿ + bⁿ = cⁿ, где n — целое число, большее 2. Теорема, простая в формулировке, оказалась дьявольски сложной в доказательстве. Математик Пьер де Ферма сформулировал эту задачу в XVII веке и, как известно, намекнул на доказательство, которое, по его словам, он нашел, заявив, что оно слишком большое, чтобы уместиться на полях учебника, в котором он писал. Многие математики пытались найти доказательство, но безуспешно. Уайлс работал над этой проблемой семь лет втайне от всех, прежде чем объявить о своем прорыве в 1993 году. Доказательства часто включают в себя длинные логические рассуждения, которые опираются друг на друга. Если в одном из шагов допущена ошибка, то все доказательство может оказаться неверным. Именно это произошло с Уайлсом, когда в его доказательстве был обнаружен изъян, на устранение которого у него и его коллеги Ричарда Тейлора ушел почти год. Формализация математических теорем — решение этой проблемы. Она выводит их из области применения ручки и бумаги и переводит в формат компьютерного кода, что позволяет машинам работать с ними, методично прорабатывая логику и выявляя любые недостатки. В центральном хранилище под названием Mathlib уже хранится 2 миллиона строк формализованных математических теорий. Ранее в этом году конференция экспертов по ИИ, компьютерщиков и математиков была проведена в Лондоне Кевином Баззардом из Имперского колледжа Лондона, который – до объявления Anthropic – работал над пятилетним проектом по преобразованию 100 страниц доказательств Уайлса и Тейлора в компьютерный код под названием Lean, чтобы его можно было формально проверить на корректность и использовать в качестве основы для дальнейших исследований. Баззард сказал тогда, что, когда его проект начинался, он был уверен в успехе, но недавние достижения в области искусственного интеллекта убедили его в том, что проект будет завершен гораздо быстрее, чем он ранее считал возможным. Заявление компании Anthropic теперь опережает эти усилия и окончательно решает проблему.