Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium

AI use, as the source states it

“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.”

Model: Gemini DeepThink, Claude Code, Aristotle, as stated