Speaker: Tianyi Xu (Peking University)
Time: 2026-02-04 15:00-18:00
Location: 1110, SIMIS
Zoom Meeting ID: 894 0536 8496 Passcode: SIMIS
Abstract:
This report reviews the development of the formalization of mathematics, from its foundations in logic and axiomatic theories to its modern implementation in computer proof assistants. It examines the theoretical motivations for formalization and the practical methods used to encode mathematical reasoning in formal systems. Emphasis is placed on a case study of the Lean proof assistant and its mathematical library, Mathlib, focusing on how the features of Lean help reduce the cost of formalization and support the translation of informal proofs into machine-checked mathematics. The report concludes with a discussion of emerging roles for AI-based tools in assisting proof development and formal mathematical reasoning.
English 
简体中文