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 — есть какие-то приятные свойства?

#задача

Друзья, начинаем потихоньку входить в режим ❤️

Первая задача 2026 года будет максимально дружелюбной.

🔸Условие: Саша составил число 2026 из 68 кубиков, как на рисунке выше. После этого он покрасил всю поверхность конструкции краской.

🔸Вопрос: у скольких кубиков оказалось покрашено ровно четыре грани?

Не торопимся. Рассуждения и вопросы принимаются в комментариях… Ответ и разбор пришлём завтра.

#задача

Ответ на вчерашнюю задачу: 62

Получить этот ответ можно, конечно, и честным перебором, аккуратно пройдясь по всем кубикам и «руками» пересчитав покрашенные грани, но это — путь сильных и смелых. Математики же, по своей натуре, люди ленивые, из-за этого и придумывают всякие умные ухищрения — как бы что сделать попроще…

У кубика 6 граней, и если он состыкован с двумя другими кубиками, то свободных граней остаётся 4, если с одним — то 5, а если с тремя — то 3, и т. д. Тем самым нам достаточно посчитать только те кубики, которые состыкованы не с двумя другими. Таких кубиков 6. А значит, ответ: 68 − 6 = 62.

❤️ Все, кто решил, — молодцы! И в качестве награды ловите бонусный факт: 2026 — счастливое число. И это не просто фигура речи.

В математике счастливыми называют числа, у которых цикличная замена числа на сумму квадратов его цифр сходится к 1. Числа, для которых процесс не заканчивается единицей, считаются несчастливыми числами и ещё называются грустными числами.

Проверим число 2026 непосредственно:

2² + 0² + 2² + 6² = 4 + 0 + 4 + 36 = 44
4² + 4² = 16 + 16 = 32
3² + 2² = 9 + 4 = 13
1² + 3² = 1 + 9 = 10
1² + 0² = 1

Убедились? 2026 — счастливое! Всего, кстати, в нашем веке счастливых годов не так много: были 2003, 2008, 2019 и будут ещё 2030, 2036, 2039, 2062, 2063, 2080, 2091, 2093.

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

🎉 — запустить последнюю хлопушку и начать уже работать...

#задача