|
Jialin Lu I am Jialin (Mike) Lu, a Computer Science Ph.D. student at Simon Fraser University, advised by Wuyang Chen. Previously, I completed my undergraduate studies at the University of British Columbia. My research focuses on AI for Mathematics and formal reasoning. I am interested in making AI reasoning verifiable and trustworthy through formal languages such as Lean, and building agentic systems that accelerate mathematical research. |
|
Publications |
|
Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang, Weiran Sun, Wuyang Chen Preprint, 2026 arXiv / project page We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. |
|
Lean Finder: Semantic Search for Mathlib That Understands User Intents
Jialin Lu, Kye Emond, Kaiyu Yang, Swarat Chaudhuri, Weiran Sun, Wuyang Chen ICLR, 2026 arXiv / project page We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. |
Miscellanea |
Teaching |
Teaching Assistant, CPSC313 (Operating Systems), UBC, 2025
Teaching Assistant, CPSC330 (Applied Machine Learning), UBC, 2024 |
|
Website design from: Jon Barron |