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

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

Organizer(s) Costas Bachas, Semyon Klevtsov, Nikita Nekrasov, Emmanuel Ullmo
Date(s) 5/9/22 - 5/13/22
linked URL https://indico.math.cnrs.fr/event/7727/
00:00:00 / 00:00:00
22 27

Dependent Type Theory from the Perspective of Mathematics, Physics, and Artificial Intelligence

By David McAllester

Dependent type theory imposes a type system on Zemelo-Fraenkel set theory (ZFC). From a mathematics and physics perspective dependent type theory naturally generalizes the Bourbaki notion of structure and provides a universal notion of isomorphism and symmetry. This comes with a universal substitution theorem --- isomorphic objects are inter-substitutable in well-typed contexts (Hofmann and Streicher 1995). From an AI perspective, or automated reasoning perspective, dependent type theory underlies the LEAN interactive verifier which is currently the go-to system for formal verification of mathematics. This talk will review dependent type theory as a discipline on set theory (the set model of type theory) and discuss approaches to improving automated reasoning based on SMT (SAT Modulo a theory) technology. This results in a class of inference algorithms under the name SAT modulo type theory or SMTT. Speculations on the relationship between SMTT and deep learning will be discussed briefly.

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