Herald: A Natural Language Annotated Lean 4 Dataset - Gao, Guoxiong; Wang, Yutong; Jiang, Jiedong; Gao, Qi; Qin, Zihan; Xu, Tianyi; Dong, Bin (International Conference on Learning Representations, 2025)