00:00:00 / 00:00:00

Appears in collection : Workshop Schlumberger : Types dépendants et Formalisation des mathématiques

A remarkable feature of logics based on typed lambda calculus is that they allow embedding functional programs in the representation of mathematical knowledge. These can be used to animate formal theories and make them behave, in part, as a working mathematician would expect. Examples of such functional encodings have played a key part in several large formal proofs, such as this of the Four-Color and Odd Order theorems.

Information about the video

  • Date of recording 6/15/22
  • Date of publication 6/20/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