Introduction to Lean

报告人：徐天一（北京国际数学研究中心）

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

地  点：海韵园实验楼S102

内容摘要:

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.

个人简介：

徐天一，现就职于北京国际数学研究中心 AI for Math 课题组，负责 Lean 4 相关工具开发。长期从事 Lean 相关开发与实践，参与开发了 Lean 4 分析工具“稷下”，在 Lean 的使用、工具开发和教学推广方面具有较丰富的经验。

联系人：马家骏