이 포지션 페이퍼는 개별 문장에 초점을 맞추는 대신 완전한 이론을 구조화된 라이브러리로 형식화하는 이론 수준의 자동 형식화를 주장합니다.

저자들은 고립된 정리 번역에서 공리, 정의, 보조정리의 전체 웹을 다루는 것으로의 전환의 중요성을 검토합니다. 그들은 대안적인 관점을 다루고 이 분야의 미해결 과제를 식별합니다.

분야를 발전시키기 위해 저자들은 이론 수준 자동 형식화를 위한 세 가지 유망한 전진 경로를 제안합니다.