Elamur Research⌕
☰
home / authors / Zenan Li

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.

5 papers in our library · 2024–2025

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

The profile is the library's match of the name; two people with one name are not always told apart.

Elsewhere: Google Scholar · Semantic Scholar · dblp · ACL Anthology

 Affiliations

From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine. 7 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. 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.
  2. 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).
  3. 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.
  4. 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…
  5. 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

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

Venues

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

 Cited by

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

Updated

↑ back to top

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