PhD student, Chinese University of Hong Kong, Shenzhen
1 paper at NeurIPS 2025
Structure-first, training-free premise selection for Lean4: CSE trees with WL screening and TED reranking that beat semantic baselines on Mathlib4.
