🧑‍🔬 Haiming Wang

🏛️ Affiliations

🎓Southeast UniversityNanjing · China1994–2026 · 198 papersEducation 1994–1999 · B.E., Department of Radio EngineeringEducation 1999–2002 · M.E., Department of Radio EngineeringEducation 2004–2009 · PhD., School of Information Science and EngineeringEmployment since 2002 · Professor, School of Information Science and Engineeringcurrent🔬State Key Laboratory of Millimeter WavesNanjing2005–2026 · 165 paperscurrent🏢LenovoBeijing · China2021–2026 · 3 paperscurrent🎓Tarim UniversityAral · China2025–2026 · 2 paperscurrent🤝Xinjiang Production and Construction CorpsÜrümqi · China2025–2026 · 2 paperscurrent🎓Beijing Union UniversityBeijing · China2026 · 1 papercurrent🔬Purple Mountain LaboratoriesNanjing · China2019–2024 · 51 papers🏢NokiaBeijing · China2005–2010 · 26 papers🔬Centro de Investigaciones en OpticaLeón · Mexico1994–1998 · 11 papers🎓Sun Yat-sen UniversityGuangzhou · China2021–2025 · 7 papers

From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine. 52 more institutions on single bylines are not listed.

🧭 Fields, topics and concepts

Of its works in our library, with the number of works on each.

📅 Works by year

2020s

📄 Papers

The most cited first (OpenAlex and our library).

1. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning (2025 · 92 citations)
   Earlier neural theorem provers for Lean 4 usually combined a language model with explicit search, such as best-first or Monte Carlo tree search.
2. LEGO-Prover: Neural Theorem Proving with Growing Libraries (2023 · 79 citations)
   Formal theorem proving is still hard for large language models. Existing LLM-based provers often fail on competition problems at middle-school level. These "plain" provers write each proof as one long monolithic block and treat the available theorem library as fixed. So a lemma proved for one problem cannot help with…
3. FIMO: A Challenge Formal Dataset for Automated Theorem Proving (2023 · 53 citations)
   Neural provers built on large language models still rarely solve olympiad-grade problems. Formal data is scarce and costly to produce, existing benchmarks contain few truly hard items, and most formal datasets lack natural-language counterparts. The authors address this with FIMO, a Lean benchmark drawn from the IMO…
4. DQ-LoRe: Dual Queries with Low Rank Approximation Re-ranking for In-Context Learning (2023 · 27 citations)
   The order and choice of demonstrations in a prompt strongly affect how well large language models solve multi-step reasoning problems.

All works

11 works of theirs in our library, the most cited first; 4 with a page here, the others link their original until we summarise them.

1. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement LearningarXiv:2504.11354Haiming Wang, Mert Unsal, Xiaohan Lin, et al.2025 · 92 citations
2. LEGO-Prover: Neural Theorem Proving with Growing LibrariesarXiv:2310.00656Haiming Wang, Huajian Xin, Chuanyang Zheng, et al.2023 · 79 citations
3. FIMO: A Challenge Formal Dataset for Automated Theorem ProvingarXiv:2309.04295Chengwu Liu, Jianhao Shen, Huajian Xin, et al.2023 · 53 citations
4. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function ↗Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) · no summary yetHaiming Wang et al.2023 · 40 citations
5. Process-Driven Autoformalization in Lean 4 ↗arXiv:2406.01940 · no summary yetJianqiao Lu et al.2024 · 33 citations
6. MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data ↗arXiv:2402.08957 (ICLR 2024 spotlight) · no summary yetYinya Huang et al.2024 · 29 citations
7. DQ-LoRe: Dual Queries with Low Rank Approximation Re-ranking for In-Context LearningarXiv:2310.02954Jing Xiong, Zixuan Li, Chuanyang Zheng, et al.2023 · 27 citations
8. Lyra: Orchestrating Dual Correction in Automated Theorem Proving ↗arXiv:2309.15806 · no summary yetChuanyang Zheng et al.2023 · 24 citations
9. TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models ↗Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing · no summary yetJing Xiong et al.2023 · 21 citations
10. CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics ↗arXiv:2505.03171 · no summary yetJunqi Liu et al.2025 · 20 citations
11. Proving Theorems Recursively ↗arXiv:2405.14414 · no summary yetHaiming Wang et al.2024 · 19 citations

🤝 Co-authors here

12 of 23 co-authors with a page, the most papers together first.

• Chuanyang Zheng ×3
• Enze Xie ×2
• Huajian Xin ×2
• Jing Xiong ×2
• Lin Li ×2
• Qingxing Cao ×2
• Yichun Yin ×2
• Zhengying Liu ×2
• Chengming Li
• Han Shi
• Jian Yin
• Jianqiao Lu

Venues

Where their works here were published, the most works first, with the editions of those that have a page.

• Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing
• Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)

🔗 Cited by

Papers of our library cite their works 402 times (of the 149,439 papers whose bibliographies we read); 41 citing papers with a page here →.

Updated 2 November 2026

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/authors/haiming-wang/