Смотрите, что придумали наши коллеги из Яндекс Образования 👀

Всю прошлую неделю они показывали, как числа живут в сервисах Яндекса и людях, которые их создают. А сейчас, в финале празднования Дня математики, нам предложили представить мир без царицы наук.

Для этого в московском ТЦ «Авиапарк» открыли, не поверите, музей вещей без математики. Как и ожидалось, внутри абсолютно пусто. Нам ли не знать, что без неё и правда ничего не заработает!

Экспозиция будет открыта ещё пару дней — если будете рядом, загляните. А сейчас смотрите видео про нашу любимую математику и ставьте 🦄, если вдохновило!

#рекомендуем

Сегодня у нас снова несложная, но любопытная задача с очень лаконичным условием:

🔄Перед вами фигура на тетрадном листе. Разрежьте её на четыре части одинакового периметра так, чтобы среди этих частей не было равных🔄

Задача точно под силу каждому, но своя изюминка в ней всё же есть. Скидывайте свои варианты под спойлером в комментарии. Решение появится завтра ❤️

#задача

⏩️️️️️ИИ решил математическую задачу, с которой человечество не могло справиться десятилетиями⏪️️️️️

В новостях всё чаще появляются подобные заголовки. Звучит впечатляюще, но стоят ли за этим полноценные научные результаты? Или всё ради хайпа? Давайте разбираться — разговор будет основательный и с пруфами!

Глава 1: Не ИИ, а алгоритмы

Повестка вокруг ИИ создаёт ощущение, что компьютерные достижения в математике — это что-то новое. Но история куда длиннее…

1️⃣Одним из первых громких случаев «компьютерного доказательства» стало решение проблемы о четырёх красках в 1976 году.

Звучит она так: любую карту можно раскрасить четырьмя цветами так, чтобы соседние области не совпадали. Доказательство оказалось настолько громоздким, что без компьютера справиться было невозможно — программа перебрала 1936 конфигураций, но математики всё равно относились к неручной работе с подозрением.

2️⃣ В конце XX века разрешилась гипотеза Кеплера о плотнейшей упаковке шаров. О ней мы, кстати, уже писали ранее тут и тут.

Она оставалась недоказанной почти 400 лет. В 1998 году Томас Хейлс заявил о доказательстве, включавшем тысячи страниц текста и гигабайты расчётов. Эксперты ошибок не нашли, но и проверить результат вручную им не удалось. Так в 2003 году родился проект FlySpeck, завершившийся в 2014-м.

3️⃣ Ещё один пример — теорема Фейта-Томпсона.

Это теорема о разрешимости конечных групп нечётного порядка. Оригинальное доказательство было опубликовано в 1963 году. Его формализация в системе Coq в 2012 году под руководством Жоржа Гонтье стала вехой в истории компьютерной проверки доказательств и заняла почти пятнадцать лет.

️️ 4️⃣ И, конечно, классификация конечных простых групп.

Грандиозный проект длиной в полвека и объёмом более десяти тысяч страниц. Здесь компьютеры играли заметную роль в доказательствах, связанных со спорадическими группами. Один из идеологов проекта, в шутку называл классификацию «тридцатилетней войной».

Эти примеры показывают: компьютеры давно участвуют в математике, но скорее как верификаторы, перебирающие варианты, проверяющие случаи и формально подтверждающие логические выводы.

Однако и искусственный интеллект в математике появился вовсе не вчера!

Глава 2: Не алгоритмы, а ИИ

Первые ИИ-системы середины XX века были символическими, логическими и уже тогда пытались рассуждать и доказывать.

1️⃣️️ Logic Theorist, родившаяся в 1956 году, была первой программой, которую создатели прямо назвали «искусственным интеллектом».

Она смогла доказать 38 из 52 теорем из Principia Mathematica. Программу представили на Дартмутской конференции 1956 года, которая считается моментом рождения ИИ как научной дисциплины.

2️⃣️️ Через год появилась GPS.

Программа General Problem Solver демонстрировала универсальный подход к решению задач — от логических головоломок и алгебраических преобразований до просчёта шахматных позиций. Проблема была лишь в том, что комбинаторный взрыв делал сложные задачи непосильными компьютеру. Тем не менее это был настоящий ИИ.

За этими программами стояла важная идея формализации математики, которая возникла задолго до компьютеров. Формализация утверждала, что любая теорема — это цепочка строго определённых логических шагов.

А это значит, что математики могли поручить машине вычисления и, главное, рассуждения, пусть и на ограниченных мощностях. Как думаете, что-то изменилось сейчас, в 21 веке?

Будем рады почитать ваши мысли в комментах. И тыкайте на 🙊, если хотите знать, что за история с заголовками, и почему она нас так волнует. Расскажем завтра!

#история

А в математике только и разговоров, что об ИИ

🔄Недавно мы написали пост о ранних попытках использовать нейронки в математике. Выбирая тему, мы наивно полагали, что историю можно рассказать всего в двух частях. Но материала оказалось куда больше. Поэтому усаживайтесь поудобнее — мы выпускаем ещё один сериал🔄

Итак, вот что происходит в математической ИИ-повестке сейчас:

▶️известные журналы посвящают теме большие статьи
▶️крупные компании выкладывают регулярно обновляемые бенчмарки
▶️наш любимчик Теренс Тао регулярно выступает на эту тему в подкастах, на лекциях, в Оксфорде и даже выделил в своём блоге хештег для ИИ-результатов

Но сама идея о самообучении программ начала зарождаться в 1950-е годы. Развивал её Артур Самуэль. Он создал программу для игры в шашки.

Задумка была по тем временам радикальной. Самуэль позволил компьютеру учиться на собственном опыте.

🔸Он играл партии, сохранял результаты и постепенно настраивал веса эвристик — оценочных функций, которые определяли, насколько «хорошей» считается позиция на доске.

🔸Обучение шло не только на успехах. Программа фиксировала и «провальные» ходы, избегая их в будущем. Так формировался примитивный механизм обучения с подкреплением — один из ключевых элементов современного ML.

🔸Шашки Самуэля доказали, что ПО может адаптироваться к сложным задачам, улучшая свои стратегии поиска решений по мере накопления опыта.

На основе этой работы были построены гугловские проекты AlphaGo и AlphaFold. В первом случае ИИ научился играть на уровне лучших игроков мира, а во втором — предсказывать пространственную структуру белков, что десятилетиями считалось сложнейшей задачей молекулярной биологии.

С появлением крупных языковых моделей (LLM) «математический» ИИ тоже перешёл на новый уровень. Например, DeepMind разработал проект FunSearch — «поиск в пространстве функций», нейронку, которая генерирует программы-решения математических задач.

Она работает, комбинируя обученную LLM (Google PaLM 2), с автоматизированным «проверяющим». Этот инструмент проверки фактов предполагает предотвращение распространения ложной информации — или, как это сейчас ещё называется, галлюцинаций.

Такой процесс позволяет преобразовывать первоначальные решения в новые знания, а также следить за тем, как строятся решения. Разработчики утверждают, что именно это и отличает FunSearch от других подобных программ.

В частности, FunSearch испытали на двух сложных математических задачах:

🔸Bin packing problem: оптимальное размещение предметов разного размера по контейнерам

FunSearch нашла стратегию, которая практически не оставляет промежутки и делает укладку более плотной, чем традиционные жадные алгоритмы.

🔸Cap set problem: поиск наибольшего множества точек на решётке, в котором никакие три точки не лежат на одной прямой

FunSearch успешно обнаружила новые конструкции для достаточно больших множеств «кэпов», которые значительно превосходят наиболее известные.

Хотя LLM не решила задачу полностью, она застолбила за собой результат, подвинув все предыдущие оценки, найденные человечеством. Так писали исследователи в громких статьях в Nature и The Guardian.

Конечно, среди математиков хватает как скептиков результативности подобных систем, доказывающих их переоценнённость, так и тех, кто продолжает регулярно анализировать результаты их математических бенчмарков и сообщать об успехах.

Друзья, и это мы ещё не дошли до самых главных открытий. Спойлер: их ещё на русском языке даже осветить не успели.

Накидайте ⚡️, если хотите быть первыми, кто узнает об этом.

#как_устроено

12 октября этого года исследователь OpenAI Себастьен Бубек опубликовал пост, в котором заявил, что GPT-5 Pro «решил» проблему Эрдёша № 339.

*️⃣Эрдёш — это математик, чью научную плодовитость нередко сравнивают с Эйлером. Он оставил после себя огромное количество открытых проблем. Сегодня они собраны на специальном сайте, отслеживающем текущий статус каждой из них, и задача № 339 на момент публикации Бубека числилась нерешённой.

▶️На самом деле новость оказалась кликбейтом: GPT-5 просто обнаружил, что эта задача уже была решена ранее. Точнее, её решение напрямую следует из одного из утверждений статьи 2003 года.

Поэтому многим не понравилось, как Бубек сформулировал своё сообщение. Создалось впечатление, что результат авторов статьи приписывается ИИ. Вероятно, на этом история могла бы и закончиться, но…

…буквально через несколько дней Бубек заявил, что GPT-5 решил ещё около десяти задач Эрдёша, включая задачу № 1043.

И вот тут-то и началось самое интересное. Пост вскоре удалили, разгорелся скандал, а Бубеку пришлось публично извиняться. Ситуацию, кстати, откомментировал даже Демис Хассабис — известный исследователь ИИ, нобелевский лауреат и по совместительству CEO DeepMind. Он сухо написал: «Как неловко».

▶️Причина скандала заключалась в следующем. Рассматривая задачу № 1043, GPT-5 обнаружил, что она была решена ещё в 1961 году Кристианом Поммеренке. Решение было «спрятано» где-то глубоко в статье, да ещё и на немецком языке.

Иными словами, «новое решение» оказалось уже известным доказательством, которое ИИ сумел извлечь из научной литературы и правильно интерпретировать. Это напрочь расходилось с анонсом результата.

❗️И всё же, несмотря на это, уже 6 задач Эрдёша изменили свой статус на «решённые» благодаря анализу ИИ.

Интересное обсуждение этих событий можно найти в треде Теренса Тао, а также в этой ветке на реддите, куда в комментарии, в частности, пришёл сам создатель базы проблем Эрдёша.

Ну как вам этот эпизод? Голосуйте в реакциях:

🦄 — Я — оптимист! Эта история показывает сильную сторону LLM. Они умеют эффективно находить, связывать и перерабатывать математические знания.
🗿— Я — скептик… Все открытия ИИ — это частично забытые или плохо индексируемые находки в рамках существующей научной литературы.

Если вам интересно, у нас есть свой ответ. Но сохраним интригу до завтра. У этой истории есть продолжение…

#история

1 декабря, то есть буквально в этом месяце, с помощью ИИ была решена ещё одна проблема Эрдёша 🤯

Она оставалась нерешённой на протяжении 30 лет. А решила её система Aristotle. Чуть подробнее о ней:

Это ИИ-система от стартапа Harmonic. Она не работает сама по себе и фигурирует лишь на одном из этапов многоступенчатого пайплайна.

▶️Одним из ключевых инструментов также является Lean — это язык программирования и система для формальной верификации математических доказательств, в которой доказательства записываются как программы и автоматически проверяются на логическую корректность. Это позволяет получать строгие, машинно-проверяемые доказательства теорем.

▶️Ещё важную роль играет проект DeepMind Formal Conjectures, который занимается систематическим переводом математических задач из естественного языка в формальные объекты, пригодные для работы в системах вроде Lean. По сути, это корпус формализованных гипотез и заготовок для будущих доказательств, с единым представлением задач, с которым могут напрямую работать ИИ-агенты.

Вот как примерно выглядят весь «конвейер» формализации, доказательства и последующей верификации результата:

1️⃣ берутся задачи из каталога Эрдёша

2️⃣ DeepMind Formal Conjectures связывает их с Lean-совместимыми формальными утверждениями и заготовками для дальнейшей формализации

3️⃣ языковые модели (вроде ChatGPT) помогают автоматизировать доработку дальнейшей формализации, генерируя дополняющие куски Lean-кода с целью привести задачу к итоговому машиночитаемому варианту

4️⃣ Aristotle работает в связке со всеми предыдущими инструментами, генерируя формальные доказательства на основе полученных формализаций; корректность каждого шага механически проверяется в среде Lean

Так вот, Aristotle полностью решил одну из версий задачи Эрдёша №124, поставленной в середине 1990-х. Сделал он это примерно за 6 часов, а формальную проверку доказательства Lean выполнил всего за минуту.

Отметим, что была решена «слабая» версия, поэтому в базе задача всё ещё числится нерешённой. Хоть эффективное доказательство и оказалось неожиданно простым, нельзя отрицать, что обнаружил его именно ИИ.

Здесь подмигиваем оптимистам, оставившим 🦄 под вчерашней публикацией.

Не проходит и суток, как один из создателей Aristotle сообщает о решении проблемы №481. Новость «взрывает» реддит. В комменты приходит автор доказательства и делится деталями работы.

🔄Оказалось, что на самом деле работа по активному привлечению Aristotle началась ещё в ноябре. Например, тогда вышло опровержение второй части проблемы №367, которое, как вы можете догадаться, проверил именно ИИ🔄

Кстати, произошло это всё с подачи математика Бориса Алексеева. Подробный рассказ из первых уст был опубликован 5 декабря.

А уже 8 декабря в блоге Теренса Тао выходит обстоятельный лонгрид о решении ещё одной проблемы — №1026. В нём можно проследить, как решение становится синтезом человеческой работы и ИИ.

Согласитесь, звучит впечатляюще! Но волнения в математическом сообществе присутствуют, что вполне понятно. Трудно представить, насколько иной станет математика в эпоху vibe proving.

И что же всё это значит❓

Можно предположить, что роль математика в будущем сместится в сторону архитектора доказательств. Человек выбирает определения, задаёт направления исследования и нажимает «пуск». Уже сейчас в соцсетях можно наблюдать, как любители экспериментируют с этой ролью и получают любопытные результаты.

Однако у этого романтизированного взгляда есть обратная сторона. В системах формализации иногда получаются доказательства, которые могут быть практически неинтерпретируемы для человека.

Хорошо ли, когда столь мощные системы получают результаты, которые мы не в состоянии понять? Решать вам!

#история

Наш новогодний сериал подходит к сказочному финалу. Этот пост мы хотим закрепить, поэтому начинаем его с перечисления предыдущих эпизодов:

▶️Как железо закалялось под ИИ
▶️Первые шаги математики в ML
▶️О задачах Эрдёша и, скорее, провале
▶️О задачах Эрдёша и, скорее, успехе

Ну и на десерт ещё одно открытие!

В октябре математик Паата Иванишвили сделал пост о том, что GPT-5 Pro нашёл контрпример к нерешённой задаче из списка открытых проблем фонда Саймонса. Уже к концу месяца он опубликовал проверенный результат и ссылку на полный чат с GPT-5 Pro, приведший к решению проблемы.

🔸Fun fact 1: каждый из вас может повторить этот трюк, даже просто закинув скриншот с проблемой в чат, вот пример.

🔸Fun fact 2: математик указал нейронку в соавторах. Потом отметку убрали — не соответствовало политике портала.

Вот такой получился сериал про ИИ в математике. Не грустите, у него точно выйдет продолжение. Но всё же растянем удовольствие.

Оставляйте ⛄️ под постом, если вам понравился наш новогодний подарок. И, конечно, ждём комментариев от тех, кто досмотрел сериал до конца. Несомненно, тут есть над чем порассуждать!

#рекомендуем

Прерываем наше ИИ-вещание по очень важному поводу: сегодня день рождения Джона Конвея ❤️

Этот легендарный математик шутил, что за всю жизнь так ни дня и не проработал — он играл. И в эти игры с головой втягивались его коллеги и многочисленные ученики.

Перечислить всё, что сделал Конвей, — задача объёмная. И нам в редакции ещё точно есть что рассказать про него самого, про его идеи и про то, где они находят отражение.

А вот небольшая подборка постов, где мы уже начали приоткрывать занавес его работ:

▶️Три правила «Жизни»
▶️Рекомендация книги Конвея и Кнута о сюрреальных числах
▶️Головоломка Конвея: задача и решение

Поздравить с днём рождения легенду — 🎉

Смотрите, какую любопытную историю мы нашли в канале data.csv 👀

Это блог нашего коллеги, Алексея Смагина, аналитика, дата-журналиста и преподавателя визуализации данных из команды Исследований Яндекса. А рассказал он нам про будущее онлайн-безопасности!

Если коротко — привычное шифрование RSA держится на любопытной математической асимметрии: умножать большие числа легко, а раскладывать их обратно — долго и сложно.

Даже суперкомпьютеры на таком месте пасуют. А вот квантовые — теоретически справляются куда быстрее. Гифка выше, например, красиво иллюстрирует, что им намного проще проверить правильность решения, сравнив длины всех путей в лабиринте.

У Лёши в канале вы найдёте интересные ещё много таких примеров аналитики и вдохновляющей инфографики. Очень рекомендуем подписаться ❤️

#рекомендуем

2025 год понемногу подходит к концу... Но хорошо, что задачки у нас не заканчиваются!

Если предновогодняя суета вас ещё не сильно затянула, предлагаем чуть отвлечься и подумать о цифрах.

Найдите все целые решения уравнения на картинке выше 🔍

Подсказку давать не будем, она и так уже содержится в условии. А вот ваши ответы с нетерпением ждём в комментах под спойлерами.

#задача

Решаем задачу и провожаем 2025 год ❤️

Можно заметить, что оба числа должны быть кратны 3. Также числа должны иметь разную чётность, причём то, которое чётное, должно делиться сразу на 4.

После этого перебор уже элементарен и даёт нам с точностью до знаков и перестановки местами пары значений 0 и 45 или 27 и 36. Тем самым всего 12 решений.

Можно было решить и чуть иначе, если заметить, что 2025 = 45². А значит, кроме тривиальных решений, остаётся проверить пифагоровы тройки с точностью до знаков. Собственно, 27, 36 и 45 — это просто масштабированный египетский треугольник.

А теперь расскажем немного о числе 2025, перед тем как уйти в новый 2026-й:

👟
👟2️⃣
👟
Как мы уже знаем, 2025 — это полный квадрат числа 45, при этом 45 можно представить как (2+0!)² × 5. Заметим, что это первый квадрат после 1936. Но интереснее всего вот что: 2025 = (20 + 25)².

Дело в том, что 45 является числом Капрекара — числом, квадрат которого можно разбить на две части, сумма которых даёт исходное число. В следующий раз такое повторится только в 3025 году, то есть через тысячу лет.

👟
👟0️⃣
👟
Числа, равные сумме первых последовательных натуральных чисел, называют треугольными. Такие, как, например, 45 = 1+2+3+4+5+6+7+8+9. А значит, 2025 = (1+2+3+4+5+6+7+8+9)² является квадратом треугольного числа.

Из предыдущего, согласно тождеству Никомаха, сразу следует, что 2025 является суммой кубов соответствующих чисел: 2025 = 1³+2³+3³+4³+5³+6³+7³+8³+9³.

👟
👟2️⃣
👟
2025 можно записать как сумму двух полных квадратов 2025 = 27² + 36² или даже как сумму трёх полных квадратов 2025 = 40² + 20² + 5².

Но можно пойти ещё дальше, задавшись вопросом: сколько имеется различных k, для которых 2025 можно записать как сумму k различных ненулевых квадратов.

Оказывается 17, причём k принимает все значения от 1 до 17. Более того, 2025 — первое число, которое имеет 17 различных значений k:

2025 = 45²
= 36² + 27²
= 35² + 28² + 4²
= 42² + 16² + 2² + 1²
= 36² + 20² + 18² + 2² + 1²
= 39² + 21² + 7² + 3² + 2² + 1²
= 43² + 11² + 5² + 4² + 3² + 2² + 1²
= 39² + 20² + 7² + 5² + 4² + 3² + 2² + 1²
= 42² + 11² + 7² + 6² + 5² + 4² + 3² + 2² + 1²
= 30² + 29² + 12² + 7² + 6² + 5² + 4² + 3² + 2² + 1²
= 40² + 11² + 10² + 8² + 7² + 6² + 5² + 4² + 3² + 2² + 1²
= 38² + 14² + 10² + 9² + 8² + 7² + 6² + 5² + 4² + 3² + 2² + 1²
= 30² + 22² + 16² + 10² + 9² + 8² + 7² + 6² + 5² + 4² + 3² + 2² + 1²
= 30² + 20² + 14² + 12² + 10² + 9² + 8² + 7² + 6² + 5² + 4² + 3² + 2² + 1²
= 25² + 23² + 14² + 13² + 11² + 10² + 9² + 8² + 7² + 6² + 5² + 4² + 3² + 2² + 1²
= 23² + 19² + 17² + 14² + 12² + 11² + 10² + 9² + 8² + 7² + 6² + 5² + 4² + 3² + 2² + 1²
= 23² + 16² + 15² + 14² + 13² + 12² + 11² + 10² + 9² + 8² + 7² + 6² + 5² + 4² + 3² + 2² + 1²

👟
👟5️⃣
👟
Если к каждой цифре числа 2025 прибавить единицу, получим число 3136. И оно тоже — полный квадрат! 3136 = 56².

Также 2025 представляется как сумма арифметической прогрессии, более точно — сумма первых 45 нечётных натуральных чисел: 2025 = 1+3+5+7+9+11+…+89.

👟
👟*️⃣
👟
В математике полнократным числом называют положительное целое число, которое делится нацело квадратом каждого своего простого делителя. И 2025 — наш клиент, поскольку 2025 = 3⁴×5². Заметим, что в этой записи используются все цифры от 2 до 5.

Можно пойти ещё дальше и сделать 1×3⁴×5², чтобы получить числа от 1 до 5, или даже 1⁶×3⁴×5²×7⁰ для чисел от 0 до 7 (с нечётными возрастающими основаниями и чётными убывающими показателями степени в качестве бонуса!).

А ещё 2025 можно записать как произведение двух полных квадратов, причём двумя способами:
2025 = 3²×15² = 5²×9², причём 5²×9² = (2−0−2−5)² × (2+0+2+5)².

Ну и напоследок — 2025 является числом Харшад. Это числа, которые делятся на сумму своих цифр. Слово Harshad пришло из санскрита: harṣa означает радость, восторг, а da — давать. То есть буквально «дающий радость».

В то же время 2025 является 454-м апокалиптическим числом. Вот и делайте выводы…

А каким числом 2025 год оказался для вас?

❤️‍🔥 — Прекрасный, несмотря ни на что!
☃️ — Может, лучше уже посмотрим, что там с 2026 — есть какие-то приятные свойства?

#задача