Poster · Sydney
LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
- When
- Tue 8 Dec 2026, 10:00–13:00 AEDT
- Where
- Hall 1-4, ICC Sydney
Exhibition Centre, Level 1 - Session
- Sydney Poster Session 1
- Authors
- Guoxiong Gao, Zeming Sun, Jiedong Jiang, Yutong Wang, jd xu, Peihao Wu, Bryan Dai, Bin Dong
- Organisations
- Peking University, Beijing International Center for Mathematical Research, Ubiquant, IQuest Research
- QRS classification
- Recommendation and retrieval