Translating Informal Proofs into Formal Proofs Using a Chain of States

Ziyu Wang, Bowen Yang, Chenyi Li +4

We address the problem of translating informal mathematical proofs expressed in natural language into formal proofs in Lean4 under a constrained computational budget. Our approach…