Towards autoformalization of textbook mathematics with natural proof checking

By Adrian De Lon — Mathematical Logic Group, University of Boon, Czech Institute of Informatics Robotics and Cybernetics Textbook mathematics relies on context and implicit reasoning, presenting its arguments in a form optimizedfor human comprehension rather than formal verification. Formal systems, in contrast, demand explicit, step-by-step arguments in a rigid syntax, which contributes to the difficulty of formalization. To bridge this gap, we propose using a controlled natural language as an intermediate representation, augmented by automated theorem provers to verify human-sized proof steps. The design of this language draws both from practical experiences with proof vernaculars of interactive theorem provers and from techniques of formal linguistics. This approach aligns naturally with LLM-based autoformalization, exploiting the vast corpus of quasiformalist mathematical texts. By isolating essential mathematical content from incidental surface details, it opens a path towards systematic modelling and verification of textbook mathematics.