00:00:00 / 00:00:00

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

By David McAllester

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

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 12/05/2022
  • Date of publication 13/05/2022
  • Institution IHES
  • Language English
  • Audience Researchers
  • Format MP4

Domain(s)

Last related questions on MathOverflow

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

Ask a question on MathOverflow




Register

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