Speaker：Tianyi Xu (Beijing International Center for Mathematical Research)

Time：2026-9-1 14:00

Location：Conference Room S102 at Experiment Building at Haiyun Campus

Abstract:

This introductory talk presents the basic concepts and use of Lean. It explains how to state mathematical propositions, inspect proof states, and complete proofs with simple tactics. Basic examples will illustrate the main steps of writing a formal proof in Lean.