Cet article de position plaide pour l'autoformalisation au niveau théorique, qui consiste à formaliser des théories complètes sous forme de bibliothèques structurées plutôt que de se concentrer sur des énoncés individuels.
Les auteurs examinent l'importance de ce passage d'une traduction de théorèmes isolés à la gestion de réseaux entiers d'axiomes, de définitions et de lemmes. Ils abordent les points de vue alternatifs et identifient les défis ouverts dans ce domaine.
Pour faire avancer le domaine, les auteurs proposent trois voies prometteuses pour l'autoformalisation au niveau théorique.