Mathematics in the Computer

Stream: general

[Mario Carneiro]

I presented a talk yesterday at the UMD Algebra-Number Theory Seminar, and the video is now up. (slides)

Mario Carneiro, Mathematics in the Computer

Abstract: The idea of using computers for checking mathematics has been around almost as long as computers themselves, but they have gradually started to see more mainstream recognition, and increasingly large and ambitious projects are being attempted in these systems. My own history with theorem provers started with the Metamath system, and then the Lean theorem prover, and it has since expanded into other theorem provers. Maintaining a formal mathematical library is very different from the mathematics they teach you in school, requiring a strange mix of programming and mathematics skills. But the experience is fun and rewarding, and the field itself is growing in relevance and popularity. Peering into the foundations of the enterprise reveals even more questions - why should we trust computers any more than humans? What can we do to make computer-powered mathematical arguments as air-tight as possible? Is it possible to build a formally verified theorem prover? How will all this affect the practice of mathematics in the future?

[Kevin Buzzard]

I just spoke at their colloquium and I mentioned Mario and someone was like "oh hey is that the guy who spoke here on Monday?"