Showing cs.CLShow all
2 papers · 1 filter
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…
cs.CL2024
Herald: A Natural Language Annotated Lean 4 Dataset
Guoxiong Gao, Yutong Wang, Jiedong Jiang +4
Verifiable formal languages like Lean have profoundly impacted mathematical reasoning, particularly through the use of large language models (LLMs) for automated reasoning. A signi…