Anthropic при помощи одной из моделей искусственного интеллекта Claude построила проверяемую на компьютере версию чрезвычайно сложного математического доказательства. Источник изображения: anthropic. com Доказательство, над которым Anthropic работала в рамках данного проекта, подтверждает гипотезу, получившую название Великой теоремы Ферма — она была выдвинута в 1637 году, и связана она со свойствами положительных целых чисел. Доказательство теоремы в 1995 году разработал математик Эндрю Уайлс (Andrew Wiles) — оно занимает 129 страниц, а на его проверку требуются несколько месяцев работы. В рамках исследовательского проекта Anthropic удалось формализовать доказательство Уайлса, то есть преобразить его в форму, которую можно проверить на компьютере. Формализованное доказательство представляет собой код, написанный на языке программирования Lean — его размер составляет 13 млн строк, и это самый большой объём за всю историю
