Formalização Semiautônoma do Equilíbrio de Vlasov-Maxwell-Landau
Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
March 16, 2026
Autores: Vasily Ilin
cs.AI
Resumo
Apresentamos uma formalização completa no Lean 4 da caracterização de equilíbrio no sistema Vlasov-Maxwell-Landau (VML), que descreve o movimento de plasma carregado. O projeto demonstra o ciclo completo de pesquisa matemática assistida por IA: um modelo de raciocínio de IA (Gemini DeepThink) gerou a prova a partir de uma conjectura, uma ferramenta de codificação agentiva (Claude Code) a traduziu para o Lean a partir de instruções em linguagem natural, um provador especializado (Aristotle) fechou 111 lemas, e o kernel do Lean verificou o resultado. Um único matemático supervisionou o processo ao longo de 10 dias a um custo de US$ 200, sem escrever uma única linha de código.
Todo o processo de desenvolvimento é público: todas as 229 instruções humanas e 213 *commits* do git estão arquivados no repositório. Relatamos lições detalhadas sobre os modos de falha da IA – como a deriva hipotética, *bugs* de alinhamento de definições e comportamentos de evitação do agente – e sobre o que funcionou: a divisão entre prova abstrata/concreta, a autorrevisão adversarial e o papel crucial da revisão humana de definições-chave e enunciados de teoremas. Notavelmente, a formalização foi concluída antes do rascunho final do artigo matemático correspondente estar terminado.
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.