Time: 9:30-16:30, May 31st-Jun 1st 2025
Venue: E10-205, Yungu campus
Agenda |
May 31st |
Topic |
9:30-10:30 |
Advancing Automated Theorem Proving: Bridging the Gap to Research-Level Mathematics (王语同，新加坡国立大学) |
10:30-11:00 |
Tea break |
11:00-12:00 |
Formalizing Gröbner Basis Theory in Lean: Towards Automated Proof via Symbolic Computation (沈皓，中国科学院大学) |
12:00-14:00 |
Lunch break |
14:00-15:00 |
Coxeter群和Hecke代数的形式化 张绍君 (厦门大学) |
15:00-15:30 |
Tea break |
15:30-16:30 |
分歧群理论的形式化 白骏杰（中国人民大学） |
Jun 1st 9:30-16:30 |
分组形式化：交换代数，p进泛函分析 |
王语同 (新加坡国立大学)
Advancing Automated Theorem Proving: Bridging the Gap to Research-Level Mathematics
Automated theorem proving (ATP) lies at the intersection of computer science and mathematics and has recently become a benchmark for evaluating large language models (LLMs). While current systems perform impressively on high school Olympiad-style problems, a significant gap remains in their ability to handle research-level mathematics, which demands deep structural understanding and sophisticated proof strategies. In this talk, I will survey the current landscape of ATP systems, examine key challenges in scaling to advanced mathematical domains, and highlight recent approaches—including our own—that aim to close this gap. I will also discuss how these systems can support the formalization community and assist in the development of machine-assisted research-level proofs.
沈皓（中国科学院大学）
Formalizing Gröbner Basis Theory in Lean: Towards Automated Proof via Symbolic Computation
This presentation explores the formalization of Gröbner basis theory in Lean 4, aiming to develop an automated proof tool that synergizes symbolic computation, theorem proving, and artificial intelligence. We will discuss:
1. Symbolic Computation Foundations: Introduce what is symbolic computation
2. Formalization Gröbner basis in Lean 4: Introduce monomial orders, division algorithm, Gröbner basis, Buchberger’s criteria and Buchberger’s algorithm
3. Tactics for Algebraic Reasoning: Introduce several tactics integrating SageMath for automated proof of algebraic problems
4. Lean, CAS and AI Integration: Prospects for Integrating Lean, CAS and AI
张绍君 (厦门大学)
Coxeter群和Hecke代数的形式化
Coxeter群是一类由反射生成的群，在几何、组合、表示理论等领域有广泛应用，且Coxeter群在mathlib4中已有形式化定义，但许多相关性质并未被形式化，如Strong Exchange property，Deletion property等。故本次报告将给出其性质的Lean4证明，给出Coxeter群上Bruhat偏序的定义，并以此为基础构造Hecke代数$\mathcal{H} (W,q)$，它的一组基是$\{T_w\}_{w\in W}$，其上乘法定义如下: 若$\ell(w)<\ell(sw)$，则$T_sT_w=T_{sw}$,否则若$\ell(w)>\ell(sw)$，则$T_sT_w=(q-1)T_w+qT_{sw}$。接下来通过定义Kazhdan-Lusztig多项式$P_{x,w}(q)$确立Hecke代数的另一组基$\{C_w\}$，称作Kazhdan-Lusztig基（还有sorry），这在几何表示论中有重要应用。
白骏杰（中国人民大学）
分歧群理论的形式化
分歧群理论是代数数论中的一项重要工具，用于刻画数域或局部域的伽罗瓦扩张中素理想的分歧行为。本次报告将介绍我们对于分歧群理论的形式化工作结果：下指标分歧群的定义及其基本性质，Herbrand函数的定义及其作为分段线性函数的相关性质，以及上指标分歧群的定义及基本性质。本次报告将重点介绍我们对相关数学概念所给出的形式化定义，以及定理的形式化陈述与数学含义的对应。
