A Semantic Search Engine for Mathlib4. - Guoxiong Gao; Haocheng Ju; Jiedong Jiang; Zihan Qin; Bin Dong 001 (EMNLP (Findings), 2024)

Herald: A Natural Language Annotated Lean 4 Dataset. - Guoxiong Gao; Yutong Wang; Jiedong Jiang; Qi Gao; Zihan Qin; Tianyi Xu; Bin Dong 001 (ICLR, 2025)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning. - Ziju Shen; Naohao Huang; Fanyi Yang; Yutong Wang; Guoxiong Gao; Tianyi Xu; Jiedong Jiang; Wanyi He; Pu Yang; Mengzhou Sun; Haocheng Ju; Peihao Wu; et al. (CoRR, 2025)