@inproceedings{li-etal-2026-learning-explore, title = "Learning to Explore the Crux in Formal Theorem Proving", author = "Li, Linhan and Cui, Wenyao and Zhang, Gong-Duo and Gu, Lihong and Zhou, Lin and Shang, Jianyun and Zhang, Huaping", editor = "Lee, Hung-Yi and Dev, Sunipa and Li, Jessy and Elliott, Desmond", booktitle = "Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing", month = oct, year = "2026", address = "Budapest, Hungary", publisher = "Association for Computational Linguistics", url = "https://aclanthology.org/2026.emnlp-main.1932/", pages = "43958--43979", ISBN = "979-8-89176-459-0" }