00:00:00 / 00:00:00

Why Explain Mathematics to Computers?

By Patrick Massot

Appears in collection : Mikefest : A conference in honor of Michael Douglas’ 60th birthday

A growing number of mathematicians are having fun explaining mathematics to computers using proof assistant softwares. This process is called formalization. In this talk, I'll describe what formalization looks like, what kind of things it teaches us, and how it could even turn out to be useful (in our usual sense of "useful"). This will not be a talk about the foundations of mathematics, and I won't assume any prior knowledge about formalization.

Information about the video

  • Date of recording 5/12/22
  • Date of publication 5/13/22
  • Institution IHES
  • Language English
  • Audience Researchers
  • Format MP4


Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow


  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
  • Get notification updates
    for your favorite subjects
Give feedback