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

Motivation

• Known: 기존에도 LEAN 4 등 proof assistant를 이용한 AI 보조 formalization 연구들이 존재했으며, 대부분 competition mathematics(IMO, Putnam)나 교과서 수준 결과, 또는 인간-AI 협업 코딩을 통한 부분적 자동화(Numina의 Brascamp-Lieb 부등식, AxiomProver의 완전 자율 증명 등)에 집중되어 있었다.
• Gap: 기존 연구들은 AI 완전 자율성, 새로운 정리/정의의 도입, hard analysis 영역에서의 대규모 코드베이스, 완전히 투명하게 공개된 개발 과정(모든 prompt·commit·log)이라는 요소들을 동시에 갖추지 못했으며, 특히 수학 논문이 완성되기 전에 formalization이 먼저 끝나는 실시간 연구 병행 사례도 드물었다.
• Why: 이 작업은 research-level 수학 결과의 formal verification이 이제 LEAN 전문성이 깊지 않은 수학자에게도 매우 저렴한 비용(약 $325)과 짧은 기간(10일)으로 접근 가능해졌음을 보여주며, AI 보조 수학 연구의 실용적 파이프라인과 실패 유형에 대한 구체적 교훈을 제공한다.
• Approach: 저자는 conjecture로부터 Gemini DeepThink가 증명을 생성하고, Claude Code가 자연어 prompt를 LEAN 4 코드로 변환하며, Aristotle이 111개 lemma를 자동으로 닫는 방식으로 human-supervised, zero-code-writing formalization 워크플로우를 구축했다.

Achievement

1. 완전한 LEAN 4 formalization: Coulomb collision을 포함한 VML 시스템의 정상상태(steady-state) 정리를 34개 파일, 1만줄 이상의 LEAN 코드로 sorry 없이 완전히 검증했다.
2. 새로운 이론 구축: MATHLIB에 존재하지 않던 Landau operator, torus 미분 구조, VML 시스템 자체를 처음부터 정의했다.
3. 새로운 수학적 결과: Coulomb 충돌과 전자기 결합을 포함하는 완전한 VML 시스템의 매끄러운 정상상태(smooth steady state) 특성화가 기존 문헌에 이 정밀한 형태로는 존재하지 않는 새로운 결과임을 제시했다.
4. 완전 공개된 연구 과정: 229개의 인간 prompt와 213개의 git commit을 모두 공개하여 재현 가능하고 투명한 AI 보조 연구 사례를 제공했다.
5. AI 실패 유형 정리: hypothesis creep, definition-alignment bug, agent avoidance behavior 등 AI 보조 formalization 과정에서 발생하는 구체적 실패 모드와 대응책(abstract/concrete proof split, adversarial self-review)을 문서화했다.

How

Figure 3. Proof dependency graph, generated with LeanBlueprint

• 물리적 시스템: 시간에 무관한 정상상태 VML 방정식(Vlasov 방정식 + Landau collision operator + Maxwell 방정식)을 정의
• 증명 아키텍처를 7단계 entropy method로 구성: H-theorem → nullspace(local Maxwellian) → transport → polynomial matching → Killing's equation → maximum principle → harmonic analysis
• Gemini DeepThink가 conjecture로부터 수학적 증명을 생성(수정 불필요)
• Claude Code가 자연어 prompt를 받아 LEAN 4 코드(정의, 정리 진술, 증명 스캐폴딩)로 번역
• Aristotle이라는 특화된 자동 prover가 111개의 개별 lemma를 사람의 개입 없이 닫음
• 단일 수학자가 핵심 정의와 정리 진술을 검토하며 감독, adversarial self-review로 오류 검출
• LEAN kernel이 최종 결과를 검증(zero sorry)

Originality

• 기존 연구들이 competition math나 교과서 결과, 혹은 부분적으로만 투명한 과정에 머문 것과 달리, hard analysis 영역의 research-level 새로운 정리를 대상으로 함
• 인간이 LEAN 코드를 전혀 작성하지 않고 AI 세 가지 도구(Gemini DeepThink, Claude Code, Aristotle)를 조합한 완전한 파이프라인을 최초로 시연
• 모든 prompt, commit, 개발 로그를 완전히 공개하여 투명성 측면에서 선행 연구들과 차별화
• 수학 논문 작성보다 formalization이 먼저 완료된 독특한 연구 병행 사례

Limitation & Further Study

• 단일 프로젝트, 단일 감독자에 의한 사례 연구로 일반화 가능성에 한계가 있으며, 다른 도메인이나 더 복잡한 정리에도 동일한 워크플로우가 적용 가능한지는 추가 검증이 필요
• definition-alignment bug가 완료 후에야 전문가 검토로 발견된 점은 AI 생성 정의의 신뢰성에 대한 우려를 남김
• Aristotle, Claude Code, Gemini DeepThink 등 특정 상용 도구에 의존하므로 재현성과 비용 구조가 도구 발전에 따라 변동될 수 있음
• 후속 연구로 더 다양한 수학 분야(예: 기하학, 정수론) 및 여러 감독자가 참여하는 대규모 프로젝트로의 확장, agent avoidance behavior에 대한 체계적 완화 기법 개발이 필요

Evaluation

총평: AI 보조 수학 연구의 실용적 가능성과 한계를 매우 투명하게 보여주는 값진 사례 연구로, formal verification의 접근성을 크게 낮추는 실질적 증거를 제시하지만 단일 사례라는 점에서 일반화에는 신중한 해석이 필요하다.