【报告摘要】 Lean is a computer programming language which is expressive enough to understand the concept of a mathematical theorem and proof. This means in practice that you can teach Lean a proof of your favourite theorem. In the last few years, some quite recent theorems of mathematics (due to Scholze, Tao and others) have been taught to Lean. I will give an overview of the area, explaining where we are and where we're going. This will be a talk suitable for mathematicians – no background in computer science will be assumed.

【报告人简介】Kevin M. Buzzard 是英国著名数学家，现任帝国理工学院教授。他专注于数论和模形式的研究，并在近年来积极推广计算机辅助证明技术。在2022年国际数学家大会（IMU）上，他的报告主要围绕计算机辅助证明和数学形式化的未来展开。Buzzard 领导的团队正在 Lean 定理证明器中推进费马大定理的形式化工作。他因其卓越的贡献获得了伦敦数学会白金汉奖 (Whitehead Prize) 和贝里克奖（Senior Berwick Prize）