Distinguished Lecture——From topology to logic and provability through Grothendieck topos theory
报告人：Laurent Lafforgue（华为拉格朗日数学与计算研究中心）
时间：2025-12-11 14:00-15:00
地点：智华楼四元厅
报告摘要: The talk will review the basic elements and features of Grothendieck topos theory as a wide generalization of the notion of space. It is flexible enough and expressive enough to allow to incarnate in topological form the semantics of all mathematics formulated in first-order geometric logic and, ultimately, of all mathematics.
The talk will focus more particularly on the notion of subtopos, a wide generalization of the notion of subspace, and its double expression in topological terms and in logical terms.
The existence of such a double expression, and the fact that the whole theory is constructive, allows on the one hand to computationally translate all provability problems into topology problems.
On the other hand, the geometric operations on subtoposes and the possibility to define and compute them with more or less accurate precision, allows to develop a subtopos-based mathematics and associated computing which is different from the more classical element-based and function-based mathematics and computing.
报告人介绍：Laurent Lafforgue is a mathematician. He worked mainly in algebraic geometry and harmonic analysis. He was awarded the Fields Medal in 2002 for his contribution to the “Langlands program”, which relates Galois Theory and Automorphic Representations Theory by applying Grothendieck’s general theories to the study of special moduli algebraic spaces discovered by Drinfeld. In the last decade, his main interest gradually shifted to Grothendieck Topos Theory. He moved to Huawei in 2021. At the Lagrange Center in Paris, which was created by Huawei but works as an academic institution, he collaborates with scientists from academia on the one hand and Huawei researchers on the other hand, especially Dr Aurélien Sagnier. He works on the development of Topos Theory, more particularly of Olivia Caramello’s Theory of “Toposes as Bridges”, and the elaboration of new forms of AI based on it.
