대규모 언어 모델(LLM)이 대화형 정리 증명기(interactive theorem prover)에서 증명 공백을 닫는 능력은 상당한 수준에 도달했지만, 검증된 정리와 재사용 가능한 라이브러리 기여 사이에는 중요한 간극이 존재한다는 연구가 arXiv(논문 번호 2606.13925)에 공개됐다. 2026년 6월 11일 제출된 이 논문은 그로텐디크(Grothendieck)의 소멸 정리(vanishing theorem) 반자율 형식화 사례를 상세히 분석한다.
연구팀이 주목한 핵심 역설은 다음과 같다. 최초 형식화 버전은 ‘sorry’ 없이 컴파일에 성공했다. sorry는 Lean 등 증명 언어에서 증명을 임시로 건너뛰는 구문으로, sorry가 없다는 것은 증명이 기계적으로 완결됐음을 의미한다. 그러나 전문가 검토 결과 정의의 부적절성, 정리의 일반성 부족, 파일 구조 문제, API 설계 결함 등 심각한 문제들이 드러났다. 이후 검토 기반 리팩터링과 압축 과정을 거쳐 2차 전문가 검토를 받았고, 전후 비교에서 뚜렷한 패턴이 확인됐다.
전후 비교가 보여준 결과는 AI 에이전트의 능력과 한계를 선명하게 갈랐다. 에이전트는 국소적이고 기계적으로 확인 가능한 피드백에는 잘 적응했다. 반면 정의를 선택하고 API를 설계하는 작업에서는 여전히 취약했다. 연구팀은 자동 형식화 평가 기준이 sorry 제거 여부에만 머물러서는 안 되며, 결과물이 전문가 검토를 견뎌내는지까지 포함해야 한다고 주장한다.
이 연구는 AI 보조 수학 연구의 품질 기준 논의에 구체적 근거를 제공한다. 컴파일 성공이라는 이진 지표가 수학 라이브러리의 장기적 유용성을 보장하지 않는다는 주장은, AI 코딩 에이전트 평가 전반에도 시사점이 크다. 특히 코드베이스 유지보수성, API 일관성, 추상화 수준 선택처럼 기계가 자동 확인하기 어려운 품질 차원에서 LLM의 한계가 두드러진다는 점에서, 사람-AI 협업 형식화 프로세스 설계에 중요한 참고 사례가 된다.
