TY  - RPRT
TI  - Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
AU  - Chengwu Liu
AU  - Yichun Yin
AU  - Ye Yuan
AU  - Jiaxuan Xie
AU  - Botao Li
AU  - Siqi Li
AU  - Jianhao Shen
AU  - Yan Xu
AU  - Lifeng Shang
AU  - Ming Zhang
PY  - 2026
UR  - https://arxiv.org/abs/2604.15839
ID  - 2604.15839
ER  -