What is Lean and what does it do?

Speaker: Prof. Kevin M. Buzzard，英国帝国理工学院

Inviter: 系统所

Title: What is Lean and what does it do?

Language: English

Time & Venue: 2024.09.05  15:00-16:00   N204

Abstract: 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.