Zenan Li
Zenan Li has 5 papers in our library, in 2024–2025, most of them on Reasoning, Language models & pretraining; often with Xian Zhang, Fan Yang, Xiaoxing Ma.
OpenAlex · ORCID · h-index 6 · 43 works · 111 citations OpenAlex, 2026-10-14
📄 5 works in our library · 🔗 Cited 83 times in our library · ⭐ Paper Stars ranking: #8465
Affiliations
Fields, topics and concepts
📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 5 worksArtificial Intelligence · 5 worksComputational Theory and Mathematics · 5 worksArts and Humanities · 1 workLanguage and Linguistics · 1 work
🧭 Topics 2Research subjects and languages the work is about.Reasoning · 5 worksLanguage models & pretraining · 1 work
Works by year
2020s
Papers
- A Survey on Deep Learning for Theorem Proving (2024 · 46 citations)
Research applying neural methods, and especially large language models, to mathematical proof has grown quickly. - Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (2024 · 19 citations)
The paper addresses a weakness in LLM-based autoformalization, the task of turning natural-language math statements into formal theorems (here, Isabelle/HOL). - Neuro-Symbolic Data Generation for Math Reasoning (2024 · 14 citations)
The paper asks whether weak LLM performance in mathematics is a basic limitation or a consequence of too little reliable training data. - Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning (2025 · 11 citations)
The paper tackles automated formal proving of elementary algebraic inequalities from math Olympiads. Pure LLM provers struggle because formal proof data is scarce and the tactic space is huge. Symbolic methods such as cylindrical algebraic decomposition scale poorly and give opaque, non-readable proofs. The authors… - Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (2025 · 7 citations)
The paper asks whether formal theorem proving in Lean 4 really requires costly RL-trained prover models. The authors return to the older Draft, Sketch and Prove (DSP) pipeline and rebuild it as DSP+, which needs no training or fine-tuning. Each stage combines neural and rule-based components:
Co-authors here
- Xian Zhang ×5
- Fan Yang ×4
- Xiaoxing Ma ×3
- Zhaoyu Li ×3
- Kaiyu Yang ×2
- Xujie Si ×2
- Yuan Yao ×2
- Chenrui Cao
- Hui Xue
- Jialiang Sun
- Logan Murphy
- Xinyi Le
Venues
Cited by
Updated
This page in Markdown → https://md.research.elamur.ai/free/en/authors/zenan-li/