Осенью 2025 появился прикольный проект Аристотель: система поиска верифицированных в Lean доказательств теорем. В марте 2026 они релизнули своего агента, доступного для всех онлайн, позволяющего вводить формулировки задач на естественном языке.
В теории групп есть известный сборник нерешенных задач, Коуровская тетрадь. Она издается регулярно с '65 года (крайнее издание вышло в День знаний 2026) и является общепризнанным средством коммуникации между ресерчерами в области. В тетрадь любой математик может отправить открытую задачу из теории групп, которая кажется ему достойной внимания. Поэтому в сборник попадают как фундаментальные задачи, носящие славу крайне трудных, так и менее значительные задачи, которые не решились по какой-то причине (например, потому что недостаточно людей думали над ними и путь решения не был замечен либо потому что opportunity cost слишком большой). 20 июля на arXiv был засабмичен препринт On Some Problems from the Kourovka Notebook четырех авторов. Все решения были найдены с помощью системы Аристотель и затем переведены авторами на человеческий язык ("деформализованы"). Этот препринт циркулировал по разным тг-чатикам и привлек наше внимание как занятный прецедент.
Параллельно с описываемыми событиями я и многие математики из близкого круга начинаем активнее пользоваться сетками в исследованиях: старые отложенные задачи получают новую жизнь, многие вещи удается сдвинуть с мертвой точки. Когда сигнатурные задачи не получается пробить, чтобы отвлечься и повысить мораль, мы апробируем сетки на разных задачах, которые кажутся прикольными (понятная постановка, вовлекающая фундаментальные понятия, или привлекательность для компьютерного перебора). К концу августа у нас накопилось какое-то количество решений. Я обсуждал с другом, что же нам с этим всем делать: по отдельности не все из них тянут на самостоятельную публикацию, а скорее на короткую заметку, но все равно хочется этим поделиться с сообществом. Мы решили сделать оммаж к работе четырех авторов и написать On Some More Problems from the Kourovka Notebook. Выбрали самые симпатичные задачки и перед дропом за еще пару ночей домайнили их количество до восьми.
Недавно выложили препринт: https://arxiv.org/abs/2608.29219. В нем пять задач из Коуровки и еще три из других источников.
Как мы пишем в работе, мотивация у нас такая: с одной стороны, сработал рефлекс публикации решений открытых задач, выработанный в пре-AI эпоху (раньше это был непосредственный способ продвигать знание, а сейчас это еще вклад в корпус текстов, на которых могут обучаться будущие модели), с другой стороны, мы хотели рассказать, как можно эффективно писать промпты и направлять сетки, если мы хотим добиться от них решения. Сейчас появляется много текстов, в которых результаты получены при активном взаимодействии с AI, а само взаимодействие редко описывается, и даже какие-то, как сейчас кажется, очевидные паттерны взаимодействия приходится переоткрывать вручную.
Я бы выделил такие инсайты (они больше относятся к "кладоискательной" математике, когда хочется понять ответ на какой-то конкретный вопрос, чем для long-term серьезных исследований — в случае последних сценарии использования совсем другие, и про них я как-нибудь напишу потом).
1. Сейчас математику умеют делать фронтир-модели (Codex ChatGPT 5.6 Sol и выше, Claude Opus 5 и выше), содержательные результаты извлечь из более слабой модели сложно. К сожалению, это не очень дешево, но из полезных соображений (опыт с ChatGPT): лучше покупать подписку за 200 баксов на x20 токенов и делить пополам с другом, чем за 100 баксов на x5 токенов. В зависимости от страны варьируется прайс, поэтому перед покупкой можно поперебирать варианты на официальном сайте.
2. Про отдельно взятую задачу имеет смысл в разных чатах просить как доказать, так и опровергнуть утверждение (даже если вы в него верите): возможно, правильный путь можно будет проще найти, когда обнаружится причина, почему контрпример не строится (впрочем, это относится и необязательно к AI-математике).
3. Если в чате долго не получается решить задачу, зачастую лучше сменить чат и начать с чистого листа (большинство решений в рамках одного чата получаются в течение не более пары часов). Причина проста: контекстное окно не слишком большое; если оно переполняется, сетка начинает его сжимать, циклиться на непродуктивных идеях, начинает меньше экспериментировать и блуждать, закапываясь в ложных путях.
4. Конечно, можно просто дать формулировку и попросить решить, иногда это работает. В противном случае подумайте, как бы вы решали эту задачу, какие были бы конкретные действия (что бы начали расписывать и какие проверки проводить), попросите сетку выполнить эти действия.
5. Нейросеть может находить неожиданные связи и искать нужные источники. Иногда она не находит нужный референс, и ей можно подсказать. Полезно просить ее скачать не просто препринт с архива, а скачать именно исходники теха и разархивировать: они почти всегда доступны на архиве, и по ним ей проще ориентироваться, чем по пдфке. Старые книжки в .djvu можно тоже просить OCR'ить в текст.
6. Стандартная практика — скормить сетке недавний текст с решением (либо новый препринт, либо что-то, что вы только что получили) и спросить, какие еще "соседние" задачи можно решить похожим методом. Иногда это может быть очень плодотворным ходом.
7. Если сетка циклится на промежуточном вопросе и не может решить его, попросите оформить его отдельно в self-contained .md-файл и скормите в соседнем чате. Так очень часто получалось сдвинуться с места. Полученное промежуточное решение также можно оформить в .md-файл и скормить в исходном диалоге.
8. Если не получается замкнуть доказательство, иногда помогает попросить концептуально взглянуть на полученные результаты и проинтерпретировать их в новом ключе.
9. Когда аргумент получен и выглядит убедительно, просите сетку оптимизировать текст, максимально упростить, оставить только самое нужное. За десяток итераций часто получается достигнуть человекопонимаемого текста, который можно осмыслить и грамотно оформить.
10. Даже если вам не нравится писать код, вы можете попросить сетку реализовать перебор или написать код для машинной проверки маленьких случаев, и она это с легкостью сделает. Если вам нравится писать код, то вы это уже знаете.
11. Сетка часто пугается, когда понимает, что вопрос открыт, и ее приходится уговаривать все равно не терять намерений думать. Тут нужно "мотивировать" ее, говорить, что нерешаемые задачи тоже решаются, просить проявлять стоические качества. Отличный козырь, если недавно вы решили смежную открытую задачу: можно показать это сетке, сказать, что ничего страшного, что задача открыта, вот недавно мы решили тоже открытую задачу. Удивительно, но это несколько раз был предпоследний промпт перед получением решения.
12. ...Пишите в комментариях свои наблюдения.
Всех с Годом знаний!