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