Projects

For Math related research, please see Publications.

Agentic Memory / Autonomous Research / Test-time Learning

  1. 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

  1. Formalization of $p$-adic representation theory, work in progress, Webpage, Dependency Graph. Shurui Liu, Zhuoni Chi, Stepan Kazanin.
  2. 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

  1. 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.