CD

ChatGPT, Deepseek, Gemini и Claude Code глазами Александра Горного

IT и технологии · 7 сентября 2026 г.

Открыть канал в MAX

Claude формализовал доказательство Великой теоремы Ферма

Claude формализовал доказательство Великой теоремы Ферма Теорема была доказана в 90-х британским математиком Эндрю Уайлсом. Сейчас Claude дали доказательство, а он разложил его на тысячи промежуточных утверждений и записал всё это на языке Lean. После этого компьютер автоматически проверил, что каждый шаг логически корректен. Claude работал в основном автономно командой из десятков агентов. Агенты написали около 13 миллионов строк Lean и доказали 29.5 тысяч промежуточных теорем. Люди давали лишь редкие подсказки. Формализация современной сложной математики раньше считалась работой на годы. Claude выполнил задачу за 11 дней. На проект ушло около 6 миллиардов выходных токенов модели, сопоставимой по уровню с Fable 5.1. https://www.anthropic.com/research/formalizing-fermats-last-theorem