기존 연구는 코딩 에이전트가 Lean 4로 고급 수학 교재를 통째로 형식화할 수 있음을 보였으나, mathlib에 이미 잘 반영된 분야에 집중하고 성공을 커널 통과(kernel acceptance)로만 측정하는 한계가 있었다. 연구진은 mathlib에 거의 없는 수치해석 교재 '상미분방정식을 위한 수치해법'을 형식화해 에이전트가 새 이론을 처음부터 구축하는 능력을 시험했다. 또한 컴파일을 넘어 형식화 품질을 의미적 정확성, Mathlib 재사용, 파일 간 재사용의 세 차원으로 LLM-as-judge 방식으로 평가하는 재현 가능한 체계를 제시했다. 이를 자신들의 형식화와 RepoProver·M2F 결과에 적용해, 불완전한 다부분 진술·약화 가설 추가·매개변수 제한 등 커널 통과로는 가려지는 불충실 형식화 패턴을 발견했다. 컴파일 기반 지표가 품질을 크게 과대평가함을 시사하며 재현 가능한 감사 방법론을 제공한다.

• •mathlib에 거의 없는 수치해석 교재를 형식화해 에이전트의 신규 이론 구축 능력 검증
• •의미적 정확성·Mathlib 재사용·파일 간 재사용의 3차원 LLM-as-judge 평가 체계 제안
• •불완전 다부분 진술·약화 가설 추가·매개변수 제한 등 커널 통과로 가려지는 불충실 패턴 발견
• •RepoProver·M2F 결과에도 적용해 공통 문제 확인
• •컴파일 기반 지표가 형식화 품질을 크게 과대평가함을 시사