3 papers
cs.LO2025
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…
cs.IR2025
MIRB: Mathematical Information Retrieval Benchmark
Haocheng Ju, Bin Dong
Mathematical Information Retrieval (MIR) is the task of retrieving information from mathematical documents and plays a key role in various applications, including theorem search in…
cs.CL2025
REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
Ziju Shen, Naohao Huang, Fanyi Yang +11
Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this pa…