🧑‍🔬 Lan Zhang

🏛️ Affiliations

🎓Clemson UniversityClemson · United States2024–2026 · 11 papersEmployment since 2024 · Assistant Professor, Electrical and Computer Engineeringcurrent🎓Michigan Technological UniversityHoughton · United States2020–2024 · 21 papersEmployment 2020–2023 · Assistant Professor🎓National University of SingaporeSingapore · Singapore2007–2025 · 14 papers🎓University of Science and Technology BeijingBeijing · China2009–2021 · 10 papers🎓Xiamen UniversityXiamen · China2009–2016 · 10 papers🎓University of Science and Technology of ChinaHefei · China2016–2024 · 9 papers🎓Harbin Engineering UniversityHarbin · China2019–2025 · 7 papers🎓Wuhan Technology and Business UniversityWuhan · China2021–2024 · 7 papers🎓University of ManchesterManchester · United Kingdom2023–2025 · 6 papers🏢China Electronics Technology Group CorporationBeijing · China2021–2024 · 5 papers

From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine. 86 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. Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning (2025 · 5 citations)
   Large language models can now translate natural-language mathematical statements into formal code (autoformalization), but checking whether such translations are actually correct is still difficult.
2. MASA: LLM-Driven Multi-Agent Systems for Autoformalization (2025 · 5 citations)
   Autoformalization is the task of turning natural-language mathematics into code that theorem provers can check.
3. FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean (2026)
   Turning informal scientific derivations into machine-checkable code is difficult. Physics adds notation such as Dirac brackets and vector calculus, which Lean's Mathlib barely supports. The authors introduce FormalScience, a domain-agnostic pipeline in which LLM agents generate statements, expand proofs, and repair…
4. VET: Verifiable Execution Tracing for Reliable Text-to-SQL Generation (2026)
   LLM-based text-to-SQL systems often hallucinate schema elements, data values or query logic. Their intermediate reasoning is either free text that nothing can check or code that runs only once at the end. VET (Verifiable Execution Tracing) is a training-free framework that replaces textual rationales with a chain of…

All works

6 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. Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions ↗Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing · no summary yetLan Zhang, Marco Valentino, Andre Freitas2025 · 11 citations
2. Consistent Autoformalization for Constructing Mathematical Libraries ↗Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing · no summary yetLan Zhang, Xin Quan, Andre Freitas2024 · 11 citations
3. Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical ReasoningarXiv:2506.10903Lan Zhang, Marco Valentino, Jordan Meadows, et al.2025 · 5 citations
4. MASA: LLM-Driven Multi-Agent Systems for AutoformalizationConference on Empirical Methods in Natural Language Processing (EMNLP)Lan Zhang, Marco Valentino, Andre Freitas2025 · 5 citations
5. FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in LeanAnnual Meeting of the Association for Computational Linguistics (ACL)Jordan Meadows, Lan Zhang, Andre Freitas2026
6. VET: Verifiable Execution Tracing for Reliable Text-to-SQL GenerationFindings of the Association for Computational LinguisticsDongyu Wang, Jingyu Li, Lan Zhang, et al.2026

🤝 Co-authors here

4 co-authors with a page, the most papers together first.

• Andre Freitas ×3
• Jordan Meadows ×2
• Marco Valentino ×2
• Liang Huang

Venues

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

• Conference on Empirical Methods in Natural Language Processing (EMNLP) ×3: EMNLP 2025
• Annual Meeting of the Association for Computational Linguistics (ACL): ACL 2026
• Findings of the Association for Computational Linguistics: Findings of the Association for Computational Linguistics 2026

🔗 Cited by

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

Updated 1 November 2026

↑ back to top

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