Shurui Liu

Recherche

Mes intérêts mathématiques portent principalement sur la théorie géométrique des représentations, la géométrie algébrique et les méthodes catégoriques dans le programme de Langlands.
Mes intérêts en informatique portent principalement sur les systèmes agentiques, l'IA pour les mathématiques (AI4Math), l'auto-formalisation et l'apprentissage par renforcement.

Mathématiques : Théorie géométrique des représentations / Langlands géométrique

  1. Automorphic Commutator Relations in Relative Geometric Langlands. Soumis, pdf, 2026.
    Déclaration d'utilisation de l'IA : avec l'aide de Rethlas et OSVerify ; pour les détails, voir l'annexe.
    Résumé

    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. En cours, brouillon disponible sur demande, 2026.
    Résumé

    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 (travail conjoint avec Zeyu Wang). Soumis, arXiv:2504.00275, 2025.
    Résumé

    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.

Mathématiques : Géométrie algébrique / Matroïdes

  1. Kazhdan–Lusztig Polynomials of Matroids Need Not Be Unimodal (travail conjoint avec Ronnie Cheng). Soumis, arXiv:2607.24186, 2026.
    Déclaration d'utilisation de l'IA : avec l'aide de Rethlas ; pour les détails, voir l'annexe.
    Résumé

    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.
    Déclaration d'utilisation de l'IA : avec l'aide de Danus ; pour les détails, voir les annexes.
    Résumé

    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. Soumis, pdf, 2025.
    Résumé

    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.

Informatique : Systèmes agentiques / 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] [mon exposé chez Cursor]
    Résumé

    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]
    Résumé

    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.

* Contribution égale.

Formalisation

  1. Formalization of $p$-adic Representation Theory. Shurui Liu, Zhuoni Chi, Stepan Kazanin. En cours. [Page web] [Graphe des dépendances]
  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. Accepté comme poster aux ateliers ICML 2026 DL4C et AI4MATH.
    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.