Type Theory and the Formalization of Mathematics: When Does Equality Compute?

报告人：董安杰（香港中文大学（深圳））

时  间：2026年9月1日 15:00

地  点：海韵园实验楼S102

内容摘要:

Dependent type theory is both a foundation for mathematics and a theory with intrinsic computational meaning. As a result, equality comes in more than one form: some equalities hold directly by computation, while others must be proved within the theory.

This talk uses the distinction between these forms of equality as a guiding theme. We will discuss how computation enters into type checking, and explore the relationships among normalization, canonicity, and extensionality.

If two objects have already been proved equal, why can we not simply treat them as computationally identical? Which mathematical facts should be built into computation itself?

个人简介：

董安杰，香港中文大学（深圳）数据科学学院在读博士生，主要研究方向为数学形式化、自动定理证明与 Lean 4。相关研究成果发表于 NeurIPS 2025，同时参与数学形式化及 Lean 定理库相关研究与实践。

联系人：马家骏