Jialin Lu

I am Jialin Lu (also go by Mike), 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, enabling LLMs to reason in formal languages such as Lean.

Email  /  Scholar  /  Github  /  LinkedIn

profile photo

Selected Publications

Lean Finder: Semantic Search for Mathlib That Understands User Intents
Jialin Lu, Kye Emond, Kaiyu Yang, Swarat Chaudhuri, Weiran Sun, Wuyang Chen
Preprint, 2025
arXiv / project page / code

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