FIMO: A Challenge Formal Dataset for Automated Theorem Proving. - Chengwu Liu 001; Jianhao Shen; Huajian Xin; Zhengying Liu; Ye Yuan 016; Haiming Wang; Wei Ju 001; Chuanyang Zheng; Yichun Yin; Lin Li; Ming Zhang 004; Qun Liu 001 (CoRR, 2023)

LEGO-Prover: Neural Theorem Proving with Growing Libraries. - Haiming Wang; Huajian Xin; Chuanyang Zheng; Lin Li; Zhengying Liu; Qingxing Cao; Yinya Huang; Jing Xiong; Han Shi; Enze Xie; Jian Yin 001; Zhenguo Li; et al. (CoRR, 2023)

MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data. - Yinya Huang; Xiaohan Lin; Zhengying Liu; Qingxing Cao; Huajian Xin; Haiming Wang; Zhenguo Li; Linqi Song; Xiaodan Liang (ICLR, 2024)

LEGO-Prover: Neural Theorem Proving with Growing Libraries. - Haiming Wang; Huajian Xin; Chuanyang Zheng; Zhengying Liu; Qingxing Cao; Yinya Huang; Jing Xiong; Han Shi; Enze Xie; Jian Yin 001; Zhenguo Li; Xiaodan Liang (ICLR, 2024)

Proving Theorems Recursively. - Haiming Wang; Huajian Xin; Zhengying Liu; Wenda Li; Yinya Huang; Jianqiao Lu; Zhicheng Yang; Jing Tang 004; Jian Yin 001; Zhenguo Li; Xiaodan Liang (NeurIPS, 2024)

DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model. - DeepSeek-AI; Aixin Liu; Bei Feng; Bin Wang 065; Bingxuan Wang; Bo Liu 039; Chenggang Zhao; Chengqi Deng; Chong Ruan; Damai Dai; Daya Guo; Dejian Yang; et al. (CoRR, 2024)

DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data. - Huajian Xin; Daya Guo; Zhihong Shao; Zhizhou Ren; Qihao Zhu; Bo Liu 039; Chong Ruan; Wenda Li; Xiaodan Liang (CoRR, 2024)

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search. - Huajian Xin; Z. Z. Ren; Junxiao Song; Zhihong Shao; Wanjia Zhao; Haocheng Wang; Bo Liu 039; Liyue Zhang; Xuan Lu; Qiushi Du; Wenjun Gao; Qihao Zhu; et al. (CoRR, 2024)

DeepSeek-V3 Technical Report. - DeepSeek-AI; Aixin Liu; Bei Feng; Bing Xue; Bingxuan Wang; Bochao Wu; Chengda Lu; Chenggang Zhao; Chengqi Deng; Chenyu Zhang; Chong Ruan; Damai Dai; et al. (CoRR, 2024)

Utilizing Natural Language Processing to Enhance Ideological Education in Tibetan Universities. - Quan Yang; Huajian Xin; Xuehua Ji; Fae Mai (Int. J. Web Based Learn. Teach. Technol., 2024)

Lyra: Orchestrating Dual Correction in Automated Theorem Proving. - Chuanyang Zheng; Haiming Wang; Enze Xie; Zhengying Liu; Jiankai Sun; Huajian Xin; Jianhao Shen; Zhenguo Li; Yu Li 006 (Trans. Mach. Learn. Res., 2024)

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search. - Huajian Xin; Z. Z. Ren; Junxiao Song; Zhihong Shao; Wanjia Zhao; Haocheng Wang; Bo Liu; Liyue Zhang; Xuan Lu; Qiushi Du; Wenjun Gao; Haowei Zhang; et al. (ICLR, 2025)

DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. - DeepSeek-AI; Daya Guo; Dejian Yang; Haowei Zhang; Junxiao Song; Ruoyu Zhang; Runxin Xu; Qihao Zhu; Shirong Ma; Peiyi Wang; Xiao Bi; Xiaokang Zhang; et al. (CoRR, 2025)

APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries. - Huajian Xin; Luming Li; Xiaoran Jin; Jacques Fleuriot; Wenda Li (CoRR, 2025)

DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. - Z. Z. Ren; Zhihong Shao; Junxiao Song; Huajian Xin; Haocheng Wang; Wanjia Zhao; Liyue Zhang; Zhe Fu; Qihao Zhu; Dejian Yang; Z. F. Wu; Zhibin Gou; et al. (CoRR, 2025)

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models. - Zhouliang Yu; Ruotian Peng; Keyi Ding; Yizhe Li; Zhongyuan Peng; Minghao Liu 003; Yifan Zhang; Zheng Yuan; Huajian Xin; Wenhao Huang 001; Yandong Wen; Ge Zhang 009; et al. (CoRR, 2025)

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving. - Luoxin Chen; Jinming Gu; Liankai Huang; Wenhao Huang 001; Zhicheng Jiang; Allan Jie; Xiaoran Jin; Xing Jin; Chenggang Li; Kaijing Ma; Cheng Ren; Jiawei Shen; et al. (CoRR, 2025)