TL;DR
Исследователь создал систему, которая за 2 недели автоматически формализовала 130k строк математики (топология из учебника) стоимостью ~$100. Механика: feedback loop — LLM генерирует формальный код → автоматический checker проверяет → ошибки возвращаются в LLM → LLM исправляет → цикл повторяется сотни раз без участия человека. Работает через coding agents (Codex, Claude Code) в изолированной среде с автоматической подачей промптов.
Ключевая находка про долгосрочную работу LLM: модель прыгает между задачами — начинает сложное доказательство, переключается на лёгкие леммы, забывает о главном, может случайно откатиться и потерять день работы. Причина: без явных правил LLM оптимизирует локально (делает что проще сейчас), а не глобально (завершает важное). Плюс ограниченная память — забывает что было в начале длинной сессии.
Решение: файл с постоянными правилами (CLAUDE.md), который читается каждый раз перед работой. В нём строгие границы ("НИКОГДА не трогай строки до 6495"), стратегия работы ("не прыгай бесконечно за лёгким"), запреты на откаты ("перед уменьшением файла — объясни почему"), приоритеты ("фокус на главных теоремах, не на упражнениях"). Плюс специальные focused prompts когда нужно срочно закончить конкретную задачу: "Вернись к доказательству леммы Урысона и закончи её. Не переключайся." Это дало 3k-строчное доказательство за день.
Схема системы
SETUP (один раз):
1. Coding agent (Codex/Claude Code) в sandbox
2. Proof checker (Megalodon) для автоматической проверки
3. Файл CLAUDE.md с постоянными правилами работы
4. Скрипт автоматизации: каждые 60 сек без изменений → подать промпт снова
ЦИКЛ (повторяется сотни раз):
Промпт: "Прочитай CLAUDE.md. Следуй инструкциям. Работай как можно дольше без остановок."
↓
LLM генерирует/исправляет код → Сохраняет backup → Запускает proof checker
↓
Checker выдаёт ошибки (или молчит = успех) → LLM анализирует → исправляет → повторяет
↓
Когда LLM останавливается (просит новый промпт) → скрипт через 60 сек подаёт тот же промпт
↓
Цикл продолжается часами (1-2 часа без участия человека)
OVERRIDE (по необходимости):
Focused prompt: "Специальное правило: вернись к [задача] и закончи. Не переключайся."
Пример применения
Задача: Пишешь большую статью про развитие нейросетей в России за 10 лет. Работаешь с Claude в Projects несколько дней. Замечаешь: модель начинает раздел про GPT-3, переключается на описание трансформеров, потом прыгает к примерам, забывает закончить анализ GPT-3. Нужно удержать фокус на главных вехах, не размазывать по деталям.
Промпт (создание файла правил):
Создай файл RULES.md для работы над статьёй. Включи:
СТРОГИЕ ГРАНИЦЫ:
- Разделы 1-3 (история до 2020) — завершены, не трогать
- Работай только в разделах 4-7 (2020-2025)
СТРАТЕГИЯ РАБОТЫ:
- Приоритет: главные вехи (выход ruGPT, Yandex GPT, GigaChat, открытые модели)
- Баланс: не застревать в технических деталях, но и не прыгать только по лёгким темам
- Перед переключением раздела: убедись что главная веха раздела раскрыта
ЗАПРЕТЫ:
- Не переписывай уже хорошие куски без явной причины
- Не удаляй заготовки — лучше временно пометь [TODO] и вернись позже
- Не дублируй информацию между разделами
МОНИТОРИНГ:
- Веди файл PROGRESS.md: статус по каждой вехе (упомянута/раскрыта/примеры добавлены/готово)
- После каждой сессии: обнови PROGRESS.md
В начале каждой сессии я буду писать: "Прочитай RULES.md и продолжай работу."
Результат: Claude создаст структурированный файл правил. В следующих сессиях ты пишешь короткий промпт "Прочитай RULES.md и продолжай работу" — модель загружает контекст правил и работает по стратегии, не размазываясь. Если нужно срочно закончить конкретную веху (например, раздел про GigaChat к дедлайну) — добавляешь focused prompt: "Специальное правило: закончи раздел про GigaChat полностью. Не переключайся на другие темы."
Почему это работает
LLM в длинных сессиях оптимизирует локально — выбирает что проще сделать прямо сейчас (описать легкую деталь, добавить пример), а не что важнее глобально (закончить сложное главное доказательство). Это как прокрастинация: начал сложную задачу → увидел лёгкую → переключился → забыл вернуться. Плюс ограниченная память в длинных диалогах — модель забывает что было 100 сообщений назад, может случайно откатиться к старой версии, потеряв полезную работу.
LLM отлично следует явным инструкциям когда они есть в контексте. Но в длинном проекте без структуры модель импровизирует стратегию на ходу — и импровизирует плохо (прыгает, размазывается, откатывается). Файл с правилами создаёт постоянную "систему координат": строгие границы ("не трогай разделы 1-3"), приоритеты ("фокус на главных теоремах"), запреты ("не удаляй заготовки"). Модель читает этот файл каждый раз → загружает стратегию работы → следует ей вместо импровизации.
Focused prompt работает как экстренное переопределение приоритетов. Обычно модель балансирует между задачами (по правилам из файла), но иногда нужно временно игнорировать баланс и закончить одну вещь до конца. Специальный промпт ("вернись к X и закончи, не переключайся") явно ставит одну задачу выше всех — модель концентрируется и доводит до конца, игнорируя соблазн прыгнуть на лёгкое.
Рычаги управления: - Границы в файле правил ("не трогай строки X-Y") → расширь если нужно переработать старое, сузь если модель лезет куда не надо - Приоритеты ("фокус на главных теоремах") → замени на свои (примеры важнее теории, детали важнее обзора) - Частота чтения правил → в исследовании читались каждый раз; в чате можешь напоминать реже или чаще - Focused override → используй для дедлайнов или когда модель застряла в прыжках
Шаблон: файл правил для долгосрочного проекта
# Правила работы над {название проекта}
## СТРОГИЕ ГРАНИЦЫ
### Что можно редактировать:
- {описание разрешённой зоны: разделы, файлы, части документа}
- Всё остальное — НЕ ТРОГАТЬ без явного разрешения
### Перед любым редактированием:
1. Проверь что работаешь в разрешённой зоне
2. Если сомневаешься — спроси перед изменением
## Правило "Не выбрасывай полезное"
1. Почти никогда не откатывайся к старым версиям
2. Если нужен откат — сначала сохрани всё полезное из текущей версии
3. В частности: сохраняй все работающие определения/куски/идеи
4. Перед уменьшением размера файла/текста: явно объясни почему и что удаляешь
## Стратегия работы
- Ты можешь делать следующее в любом порядке, но всегда должен быть прогресс:
- {тип работы 1}: {что делать}
- {тип работы 2}: {что делать}
- {тип работы 3}: {что делать}
- Важные принципы:
- **Баланс простого и сложного**: делать лёгкое ОК, но не прыгай бесконечно избегая трудного
- **Приоритет главному**: {опиши что главное в проекте} — фокусируйся на этом даже если сложно
- **Обзор всех частей**: {если проект большой} — не застревай в одной части надолго, помни обо всём проекте
- Используй постепенный подход для сложных задач: {как разбивать сложное}
## Мониторинг прогресса
- Веди файл PROGRESS: {что отслеживать}
- Формат: {как структурировать статус}
- Используй PROGRESS чтобы найти что отстаёт и переключить фокус
## Проверка работы
- После {каких изменений} запускай {какую проверку}
- Делай пронумерованные backup-ы: backup_001, backup_002, и т.д.
- С каждым backup создавай файл CHANGES_001 с кратким описанием что изменилось
- Нумерация должна только расти, не перезаписывай старые backup-ы
Как заполнить:
- {название проекта} — твой проект
- {разрешённая зона} — где модель может работать (разделы 4-7, файлы X-Y, определённая тема)
- {тип работы 1/2/3} — виды работы в проекте (написание разделов, проверка фактов, добавление примеров)
- {что главное} — приоритет проекта (главные аргументы статьи, ключевые функции продукта, основные концепции)
- {что отслеживать} — метрики прогресса под твой проект
Применение в чате
ChatGPT Projects: 1. Создай Project для долгосрочной задачи 2. Загрузи файл RULES.md с правилами работы 3. В начале каждой сессии: "Прочитай RULES.md из файлов проекта и продолжай работу по инструкциям" 4. Модель загрузит правила и будет следовать стратегии 5. Для срочных задач: "Специальное правило сегодня: {задача}. Не переключайся пока не закончишь. Остальные правила из RULES.md сохраняются."
Claude Projects (аналогично): Добавь RULES.md в Project Knowledge → ссылайся в промптах
Без Projects (обычный чат): - Вставь правила в первое сообщение длинного диалога - Периодически напоминай: "Помнишь правила работы из начала диалога? Продолжай по ним" - Минус: при длинном диалоге правила выпадут из контекста
Focused override когда нужно:
Специальное правило: вернись к {конкретная задача/раздел/доказательство}
и закончи полностью. Не переключайся на другое пока не завершишь.
Остальные правила из RULES.md продолжают действовать.
Почему длинные правила работают
В исследовании файл CLAUDE.md занимал ~250 строк с детальными правилами, запретами, стратегиями. Можно подумать что это перегружает модель, но результат показывает обратное: чем детальнее правила, тем меньше импровизации, тем стабильнее работа.
Модель хорошо обрабатывает структурированные инструкции любой длины (в пределах контекста). Детальность снимает двусмысленность: "баланс простого и сложного" можно интерпретировать по-разному, а "не прыгай бесконечно между лёгкими задачами, если не продвинулся по главным теоремам за N попыток" — конкретно. Чем конкретнее → тем предсказуемее поведение.
В твоих проектах: не бойся детализировать правила. Лучше явный список из 10 пунктов "что делать / не делать", чем один расплывчатый принцип.
Ограничения
⚠️ Применение: Эти принципы работают для долгосрочных проектов с файлами и множеством итераций. Для разовых вопросов в чате ("напиши email", "объясни концепцию") — избыточно.
⚠️ Автоматизация: Исследование использовало скрипты для автоподачи промптов и мониторинга. В обычном чате ты подаёшь промпты вручную — это добавляет барьер для очень длинных проектов (десятки часов непрерывной работы).
⚠️ Проверка качества: В исследовании был автоматический proof checker (находил ошибки сразу). В твоих задачах проверку качества делаешь ты или другие инструменты — feedback loop медленнее.
⚠️ Context window: Файл правил съедает часть контекста. Если проект огромный + правила длинные + история диалога большая → модель может упереться в лимит контекста раньше. Решение: периодически начинай новый чат с правилами + кратким резюме прогресса.
⚠️ Стоимость длинных сессий: Исследование потратило ~$100 за 2 недели активной работы на ChatGPT Pro ($200/мес). Если твой проект требует десятки часов генерации → следи за расходом лимитов подписки.
Ресурсы
130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? Репозиторий с результатами формализации: https://github.com/megalodon-prover/mgwiki Josef Urban, AI4REASON и University of Gothenburg Январь 2026