Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4.

Chengwu Liu, Yichun Yin, Ye Yuan, Jiaxuan Xie, Botao Li, Siqi Li, Jianhao Shen, Yan Xu, Lifeng Shang, Ming Zhang

Browse the full ACL paper archive.