Полуавтономная формализация равновесия Власова–Максвелла–Ландау
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
March 16, 2026
Авторы: Vasily Ilin
cs.AI
Аннотация
Мы представляем полную формализацию в Lean 4 характеристики равновесия в системе Власова-Максвелла-Ландау (ВМЛ), описывающей движение заряженной плазмы. Данный проект демонстрирует полный цикл исследований с ИИ-ассистентом: модель логического вывода (Gemini DeepThink) сгенерировала доказательство из гипотезы, агент-кодер (Claude Code) перевел его в Lean из prompts на естественном языке, специализированный провер (Aristotle) закрыл 111 лемм, а ядро Lean верифицировало результат. Единственный математик курировал процесс в течение 10 дней при стоимости в \$200, не написав ни строчки кода.
Весь процесс разработки является публичным: все 229 человеческих промптов и 213 коммитов git архивированы в репозитории. Мы сообщаем о детальных наблюдениях относительно типичных сбоев ИИ — креп гипотез, баги согласования определений, поведение уклонения агентов — и о том, что сработало: разделение доказательств на абстрактные и конкретные, адверсариальный самоанализ и критическая роль человеческого ревью ключевых определений и формулировок теорем. Примечательно, что формализация была завершена до окончания финального черновика соответствующей математической статьи.
English
We present a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, which describes the motion of charged plasma. The project demonstrates the full AI-assisted mathematical research loop: an AI reasoning model (Gemini DeepThink) generated the proof from a conjecture, an agentic coding tool (Claude Code) translated it into Lean from natural-language prompts, a specialized prover (Aristotle) closed 111 lemmas, and the Lean kernel verified the result. A single mathematician supervised the process over 10 days at a cost of \$200, writing zero lines of code.
The entire development process is public: all 229 human prompts, and 213 git commits are archived in the repository. We report detailed lessons on AI failure modes -- hypothesis creep, definition-alignment bugs, agent avoidance behaviors -- and on what worked: the abstract/concrete proof split, adversarial self-review, and the critical role of human review of key definitions and theorem statements. Notably, the formalization was completed before the final draft of the corresponding math paper was finished.