The LLM Era Demands Natural-Language-Aligned Theorem Provers for Mathematics

Traditional theorem provers were envisioned to serve multiple purposes: formalizing state-of-the-art mathematical research to ensure result reliability, developing educational tools to provide students with better feedback, and acting as formal verifiers to enhance large language models' mathematical capabilities. However, their actual performance has fallen short of expectations in practice. We analyze the challenges faced by these scenarios, and propose that the root of these issues lies in the fact that traditional theorem provers were originally designed with a focus solely on verifying logical rigor rather than representing the process by which humans conduct mathematical proofs using natural language. This fundamental design choice creates a significant gap between existing formal proof processes and informal proofs, causing both human and LLMs to expend substantial resources on handling the provers' technical details rather than focusing on key mathematical insights. Therefore, this paper advocates for the design of a new generation of theorem provers featuring proof languages that resemble natural language, capable of aligning informal and formal processes. Thereby harnessing the advanced natural language processing capabilities of the LLM to enable theorem provers to achieve their full potential across the aforementioned scenarios.