ИИ-математики снова взбудоражили ленту, и на этот раз всё выглядит почти как прорыв. Почти.
Стартап Harmonic выкатил новость: их система Aristotle якобы решила одну из задач из списка Эрдёша — №124. Это не какая-то скучная теоремка, а проблема, которая с конца 90-х висела нерешённой — впервые сформулированная в Acta Arithmetica. Человеческая математика — 30 лет. Aristotle — 6 часов. Без участия людей. Красиво.
Что вообще делает Aristotle? Это не «пишу вам текст про математику, как ChatGPT». Он работает в среде Lean — формальной системе доказательств. То есть не просто генерирует рассуждения словами, а пишет доказательства, которые можно автоматически проверить програмно. Такой гибрид из formal verification, поиска и логических рассуждений. Инструмент действительно интересный, и если вы математик — вы должны занервничать хотя бы слегка.
Но дальше случилось то, что случается всегда. Выяснилось, что решённая задача не оригинальная формулировка Эрдёша, а упрощённая версия. В ней можно начинать повышение степени с единичной и это сильно облегчает математику. В настоящей версии она недоступна и там проблема до сих пор открыта. Короче: Aristotle решил не то, но рядом.
И вот тут начинается главное. Да, машины уже умеют решать «новую» математику. Но пока — только ту, что лежит в зоне «средний аспирант справился бы». До Римана, Коллатца — ещё далеко. Сейчас это генерация «логичных шагов» по базе известных фактов. А не рождение новых идей.
Но даже если это «низко висящие плоды», важно другое: впервые появилось ощущение, что рядом с «vibe coding» появляется новый жанр — vibe proving. Математика как код. А исследования — как деплой. И когда математик сидит и разгоняет идею, рядом может быть кто-то или что-то, кто докажет за него.
В этом и есть нерв момента: формальная математика становится не профессией, а интерфейсом. А если так, то весь академический мир может поменяться ещё быстрее, чем мы думаем.
Великие математические теории ещё не побеждены ИИ. Но впервые им стало немного тревожно.
И это куда важнее, чем очередной заголовок о прорыве.
#математика #ИИ #vibeproving
