Projects
For Math related research, please see Publications.
Agentic Memory / Autonomous Research / Test-time Learning
- Automated Conjecture Resolution with Formal Verification. Haocheng Ju*, Guoxiong Gao*, Jiedong Jiang*, Bin Wu*, Zeming Sun*, Shurui Liu*, Leheng Chen, Yutong Wang, Yuefeng Wang, Zichen Wang, Wanyi He, Peihao Wu, Liang Xiao, Ruochuan Liu, Bryan Dai, Bin Dong. [Arxiv] [Rethlas] [Archon].
* Equal contribution.
Lean Project
- Formalization of $p$-adic representation theory, work in progress, Webpage, Dependency Graph. Shurui Liu, Zhuoni Chi, Stepan Kazanin.
- VeriBench: End-to-End Formal Verification Benchmarkfor AI Code Generation in Lean 4, work in progress. Joint work with Brando Miranda, Zhanke Zhou, Allen Nie, et al.
Course Project
- Dynamic Ledger: Retrieval-Augmented Structured Memory for Test-Time Learning, Jerry Gu*, Shurui Liu*, Sabrina Yen-Ko*, mentored by Mirac Suzgun, Webpage. CS224N 2025 winter.