В данной позиционной статье обосновывается необходимость автоматической формализации на уровне теорий, которая предполагает формализацию целостных теорий в виде структурированных библиотек, а не сосредоточение внимания на отдельных утверждениях.
Авторы исследуют значение этого перехода от изолированного перевода теорем к обработке целых сетей аксиом, определений и лемм. Они рассматривают альтернативные точки зрения и выявляют открытые проблемы в этой области.
Для развития направления авторы предлагают три перспективных пути развития автоматической формализации на уровне теорий.