Automatic Verification of Mathematical Texts

Most of mathematical knowledges are written in texts, and the correctness of mathematical proofs and calculations is usually established through manual check and verification, which often requires professional knowledge and takes effort. Therefore, how to verify the human-written mathematical texts automatically is always a problem to overcome. Nowadays, formal languages, e.g., Lean, Isabelle/HOL, Coq, are used to formalize mathematical knowledges, and various automated or interactive tools are proposed for verification and calculation[1], but it is still required for experts to make a formalization for these manually written text first. Some researchers attempt to use machine learning methods [2] and large language models [3] to automate the transformation from mathematical texts to formal representations, but the accuracy is still insufficient to support automated verification. To achieve the automatic verification of mathematical texts, this paper proposes an autoformalization-based verification framework for mathematical proofs.