Topic: Mathematics in the Computer
Mario Carneiro (Apr 28 2021 at 02:45):
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 (Apr 28 2021 at 20:55):
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?"
Last updated: Aug 03 2023 at 10:10 UTC