作者位次 #4/10ACL 2026Poster· Natural Language Processing
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
摘要
Most ATP benchmarks embed the final answer within the formal statement — a convention we call “Easy Mode” — a design that simplifies the task relative to what human competitors face and may lead to optimistic estimates of model capability.We call the stricter, more realistic setting “Hard Mode”:...