刘抒睿

研究

我的数学兴趣主要在于几何表示论、代数几何以及Langlands纲领中的范畴化方法。
我的计算机科学兴趣主要在于智能体系统、AI4Math、自动形式化以及强化学习。

数学：几何表示论 / 几何Langlands

  1. Automorphic Commutator Relations in Relative Geometric Langlands。已投稿，pdf，2026。
    AI 使用声明：借助 Rethlas 和 OSVerify 完成；详见附录。
    摘要

    We prove the automorphic commutator relation conjecture of Liu–Wang [LW26, Conjecture 4.45]. The proof uses the stack of formal multidisks with two ordered marked sections and constructions of objects and moduli spaces analogous to those in local relative Langlands.

  2. Modular Representation Theory via Crystalline D-modules. 进行中，草稿可应要求提供，2026。
    摘要

    We develop a six-functor formalism of crystalline $\mathscr{D}$-modules (in the sense of Bezrukavnikov–Mirković–Rumynin) on smooth schemes and smooth Artin stacks in characteristic $p>0$ and then construct a crystalline Deligne–Lusztig induction functor from the finite Hecke category $\mathscr{D}^{\mathrm{ren}}(B\backslash G/B)$ to modular representations of a finite group of Lie type in defining characteristic. We show that this functor factors through a categorical trace via formalism in Zhu (2025). As a main result, we prove it is fully faithful and its monodromic enhancement (passing through $\mathscr{D}^{\mathrm{mon}}(U\backslash G/U)$) yields an equivalence of categories, and hence provides a framework to understand modular representations via the trace category of the finite (monodromic) Hecke category.

  3. Higher Period Integrals and Derivatives of L-functions（与王泽宇合作）。已投稿，arXiv:2504.00275，2025。
    摘要

    We propose a geometric framework to produce a formula relating higher period integrals to higher central derivatives of $L$-functions over function fields, extending the framework of Ben-Zvi–Sakellaridis–Venkatesh to higher derivatives. For a strongly tempered affine smooth $G$-variety $X$, we give a geometric construction of the action of $L$-observables on the geometric period integral $\int_{X}\mathbb{L}_\sigma$ of a Hecke eigensheaf $\mathbb{L}_\sigma$ on $\mathrm{Bun}_G$. By taking a suitable version of Frobenius trace of this action, we recover higher central derivatives of the $L$-function attached to the dual symplectic representation. As an application, in the Rankin–Selberg case $(\mathrm{GL}_n\times\mathrm{GL}_{n-1},\mathrm{GL}_{n-1})$, we obtain a formula for higher derivatives of the Rankin–Selberg $L$-function. This provides a conceptual generalization of the higher Gross–Zagier formula of Yun–Zhang to higher-dimensional spherical varieties.

数学：代数几何 / 拟阵

  1. Kazhdan–Lusztig Polynomials of Matroids Need Not Be Unimodal（与Ronnie Cheng合作）。已投稿，arXiv:2607.24186，2026。
    AI 使用声明：借助 Rethlas 完成；详见附录。
    摘要

    We construct, over every finite field, representable matroids whose Kazhdan–Lusztig polynomials are not unimodal. In particular, the conjectures that all Kazhdan–Lusztig polynomials of matroids are log-concave and that they are real-rooted are both false. Our examples are obtained by deleting points from finite projective geometries. More generally, we prove that, under a half-rank degree condition in each contraction quotient, the Kazhdan–Lusztig polynomial of every contraction enumerates the subspaces whose projective points lie in the corresponding deleted set, while the $Z$-polynomial agrees with that of the full projective geometry.

  2. Tangent Classes of Matroids and Wonderful Compactifications. Ronnie Cheng, Shurui Liu, Guoxiong Gao. arXiv:2607.05835，2026。
    AI 使用声明：借助 Danus 完成；详见附录。
    摘要

    We use Danus to autonomously reproduce the main part of Ronnie Cheng's paper arXiv:2606.22650 without human guidance, before arXiv:2606.22650 was publicly available. This demonstrates the potential of AI agents in mathematical research.

  3. Künneth Formula for Étale Fundamental Groups in Characteristic 0。已投稿，pdf，2025。
    摘要

    In this article, we provide a purely algebraic proof that the étale fundamental group is invariant under base change of algebraically closed fields of characteristic 0. As a corollary, we obtain the Künneth formula for étale fundamental groups in characteristic 0. We also explain how to adapt the proof (using alterations) to apply to prime-to-$p$ fundamental groups in characteristic $p>0$. These results are known to experts, but proofs do not seem to be documented in the literature, so for convenient citation by others we are providing them in a written form here.

计算机科学：智能体系统 / AI4Math

  1. Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory. Jihao Liu, Guoxiong Gao, Zeming Sun, Bin Wu, Shurui Liu, Jiedong Jiang, Haocheng Ju, Leheng Chen, Ronnie Cheng, Xiping Zhang, Bin Dong. arXiv:2607.06447，2026。[Danus] [我在 Cursor 的报告]
    摘要

    Recent LLM-based mathematical reasoning agents have begun to tackle research-level problems and, in several cases, have contributed to the resolution of open problems. However, scaling and orchestrating such agents effectively remains challenging, due to the difficulty of coordinating parallel proof search while keeping intermediate claims organized and reliable. In this paper, we propose Danus, an orchestration system for research-level mathematical reasoning centered on a shared fact graph as a global memory-management mechanism. Danus consists of a main agent that performs planning and coordination, multiple worker agents that carry out proof search in parallel, and a stateless verifier that checks proposed mathematical claims before they are admitted into the fact graph. Each verified fact is stored together with its proof and logical dependencies, allowing the system to build long arguments incrementally while keeping the shared proof state organized. The main agent periodically summarizes the evolving proof state, redirects workers across promising directions, and supports interaction with human mathematicians through progress reports. We evaluate Danus through six research-level case studies in algebraic geometry, singularity theory, and combinatorics, illustrating how the fact-graph memory mechanism enables Danus to construct long, detailed mathematical proofs. Our results suggest that fact-graph-based orchestration provides an effective route toward scaling mathematical reasoning agents for long-horizon research problems. Danus is open source at https://github.com/frenzymath/Danus.

  2. 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:2604.03789，2026。[Rethlas] [Archon]
    摘要

    Recent advances in large language models have significantly improved their ability to perform mathematical reasoning, extending from elementary problem solving to increasingly capable performance on research-level problems. However, reliably solving and verifying such problems remains challenging due to the inherent ambiguity of natural language reasoning. In this paper, we propose an automated framework that integrates natural language reasoning with formal verification to tackle research-level mathematical problems. Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon. Rethlas combines reasoning primitives with our theorem search engine, Matlas, to explore solution strategies and construct candidate proofs. Archon, equipped with LeanSearch, translates informal arguments into formalized Lean 4 projects through task decomposition, iterative refinement, and automated proof synthesis, ensuring machine-checkable correctness. Using this framework, we resolve an open problem in commutative algebra and formally verify the resulting proof in Lean 4 with essentially no human involvement. Additional case studies illustrate the capabilities of Rethlas in informal mathematical reasoning and discovery, as well as the ability of Archon to formalize research-level proofs in Lean 4. Our experiments demonstrate that strong theorem retrieval tools enable the discovery and application of cross-domain mathematical techniques, while the formal agent can autonomously fill nontrivial gaps in informal arguments. More broadly, our work illustrates a promising paradigm for mathematical research in which informal and formal reasoning systems, equipped with theorem retrieval tools, operate in tandem to produce verifiable results, reduce human effort, and support human-AI collaborative mathematical research.

* 同等贡献。

形式化

  1. Formalization of $p$-adic Representation Theory。Shurui Liu, Zhuoni Chi, Stepan Kazanin。进行中。[网页] [依赖图]
  2. VeriBench: An End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4. Brando Miranda, Srivatsava Daruru, Ethan S. Hersch, Zhanke Zhou, Allen Nie, Daneshvar Amrollahi, Leni Aniva, Iddah Mlauzi, Kirill Acharya, Elyas Obbad, Dilara Soylu, Weston Kirk, Zixiao Jolene Wang, Kai Fronsdal, Ying Li, Donald Poindexter Jr., Rakshit Kaushik, Shurui Liu, Yegor Denisov-Blanch, Steven Dillmann, Simon Obstbaum, Santiago Cuellar, John Sarracino, Rylan Schaeffer, Mo Tiwari, Donghyun Lee, Bo Han, Sanmi Koyejo. 已作为海报被 ICML 2026 DL4C 与 AI4MATH workshop 接收。
    TL;DR

    VeriBench introduces a benchmark for evaluating language models on end-to-end Lean 4 code verification, showing current models struggle while self-optimizing agents demonstrate meaningful progress toward provably correct software generation.