수학자가 AI 시스템을 지휘해 비선형 Vlasov 방정식의 적정성(well-posedness)을 Lean 4로 완전 형식화한 사례 연구로, 이 과정을 '형식화 게임'으로 규정했다. LaTeX 논문을 sorry 없이 컴파일되고 Lean 기초 공리에만 의존하는 개발로 옮기면 승리이며, Dobrushin 평균장 경로를 통한 존재성·유일성·안정성 추정·평균장 극한까지 공리 청정하게 증명했다. 사람은 정의 범위 설정과 분해 방향 지시만 맡고 증명 작성은 AI가 수행했으며, 헤드라인 정리는 약 1주, 전체는 약 1달이 걸렸다. 부산물로 Wasserstein-1 거리와 Kantorovich-Rubinstein 쌍대성 등 최적수송 라이브러리(전체 299개 선언 중 49개)가 Mathlib에 흡수 가능한 독립 계층으로 분리돼, AI 보조 수학 형식화의 실용성을 보여준다.
- •수학자가 방향만 지시하고 AI가 증명을 작성하는 '형식화 게임' 방법론 제안
- •비선형 Vlasov 방정식의 적정성을 Lean 4로 공리 청정(axiom-clean)하게 완전 형식화
- •핵심 정리는 약 1주, 전체 개발은 약 1달 소요
- •최적수송 이론 부분(299개 중 49개 선언)이 Mathlib 호환 독립 계층으로 분리돼 재사용 가능
A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game
본문 미리보기
arXiv:2607.08986v1 Announce Type: new Abstract: We formalize a research result in the Lean 4 proof assistant by having a mathematician direct an AI system, and frame the activity as a formalization game. The objective is to turn a LaTeX document into Lean. The game is won when the development compiles, contains no sorry, and a machine check shows the target theorems rest on Lean's foundational axioms alone. Reuse is a second check, by a definition we introduce: whether the development yields a
전체 내용이 궁금하다면?
원문을 직접 읽어보세요