Max Zeuner: Constructive Mathematics and the Computational Content of Proofs
Note that this seminar is going to be an online meeting using Zoom. Feel free to join.
Time: Wed 2020-03-25 14.00 - 15.00
Participating: Max Zeuner
Mathematical proofs do not only convey the truth of certain mathematical statements, they can also carry computational content. If we want to prove that a mathematical object with a certain property exists, we might assume that no object has the property in question and try to derive a contradiction from that assumption. But we could also try to explicitly construct an example of an object satisfying the property. Only a proof following the latter strategy has computational content as it describes an algorithm for finding the object we're after, while the former strategy provides no such thing. Constructive mathematics can be seen as a way of doing mathematics that that ensures the computational meaning of all its definitions and proofs. In this talk we want to sketch the development of constructive mathematics, look at the unique perspective it gives on the notion of a mathematical proof and indicate how this ultimately led to the development of proof-assistants like Coq, Agda or Lean, powerful computer tools for verifying formalized proofs and extracting their computational content.