자연어 수학을 기계 검증 가능한 형식 언어로 옮기는 자동형식화(autoformalization)를 개별 명제 단위가 아니라 이론(theory) 단위로 확장하자고 주장하는 포지션 논문이다. 실제 형식화 작업은 목표 정리를 서술하기 전에 공리·정의·보조정리로 얽힌 전체 의존망을 먼저 구축해야 하므로, 완전한 이론을 구조화된 라이브러리로 형식화하는 방향 전환이 필요하다고 논증한다. 이 전환의 의의를 검토하고 반대 견해에 답하며, 미해결 과제와 세 가지 유망한 연구 경로를 제안한다. 관련 서베이는 GitHub(Awesome-Autoformalization)에 공개했다. LLM 기반 정리 증명이 실제 수학 라이브러리 규모로 나아가려면 필요한 문제 재정의라는 점에서 의미가 있다.

• •개별 명제 중심의 자동형식화를 공리·정의·보조정리의 의존망을 포함한 이론 단위 형식화로 확장하자는 포지션 논문
• •실제 형식화 작업은 목표 정리 서술 전에 전체 지식 기반 구축이 선행돼야 함을 근거로 제시
• •방향 전환의 의의 검토, 대안적 견해 반박, 미해결 과제 정리와 함께 세 가지 연구 경로 제안
• •자동형식화 서베이를 GitHub 'Awesome-Autoformalization' 저장소로 공개