Kevin Buzzard: "What is the point of Lean's maths library?"

12th of August, 2021. Part of the Topos Institute Colloquium.
-----
Abstract: Lean is a computer proof checker developed by Microsoft Research. Over the last four years I have been part of a team of mathematicians and computer scientists who have got it into their heads that it is somehow "obviously" a good idea to build a formally verified library of modern mathematics in Lean. You can think of it as a 21st century Bourbaki if you like, although our plans are actually far grander than Bourbaki's. I will talk about two things: (1) how it's going and (2) why we're doing it. No background in computer proof checkers will be necessary to follow the talk.

[@madvorakCZ]

Thank you for this beautiful talk!

[@markuspfeifer8473]

next up: 1. group classification theorem 2. mochizuki's "proof" of the ABC conjecture

[@thereGoMapo]

it's also a shame that a lot of the formalization work is split across other projects and programming languages. Having to build the library from scratch is tedious... There should be some common format/standard that all other projects can use and re-use.

[@thereGoMapo]

The syntax of Lean feels too clumsy.

[@1330m]

so good interesting . Longitude 127 Seoul Okinawa Soul Axis -- Bahai Faith Rael Jesus Huh kyung young Great veritas .