Lean Workbook: A large-scale Lean problem set formalized from natural language math problems. - Huaiyuan Ying; Zijian Wu 002; Yihan Geng; Jiayu Wang; Dahua Lin; Kai Chen 026 (NeurIPS, 2024)

InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning. - Huaiyuan Ying; Shuo Zhang 022; Linyang Li; Zhejian Zhou; Yunfan Shao; Zhaoye Fei; Yichuan Ma; Jiawei Hong; Kuikun Liu; Ziyi Wang 006; Yudong Wang 002; Zijian Wu 002; et al. (CoRR, 2024)

LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover. - Zijian Wu 002; Jiayu Wang; Dahua Lin; Kai Chen 026 (CoRR, 2024)

InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems. - Zijian Wu 002; Suozhi Huang; Zhejian Zhou; Huaiyuan Ying; Jiayu Wang; Dahua Lin; Kai Chen 026 (CoRR, 2024)