• Doing Mathematics with Simple Types: Infinitary Combinatorics in Isabelle/HOL

    https://youtu.be/LZMtQNdqtvc Speaker: Lawrence Paulson, University of Cambridge Computer Laboratory Title: Doing Mathematics with Simple Types: Infinitary Combinatorics in Isabelle/HOL Abstract: Are proof assistants relevant to mathematics? One approach to this question is to explore the breadth of mathematical topics that can be formalised. The partition calculus was introduced by Erdös and R. Rado in 1956 […]

  • CMSA Math-Science Literature Lecture: Isadore Singer’s Work on Analytic Torsion

    Virtual

    Edward Witten (IAS) Title: Isadore Singer’s Work on Analytic Torsion Abstract:  I will review two famous papers of Ray and Singer on analytic torsion written approximately half a century ago. Then I will sketch the influence of analytic torsion in a variety of areas of physics including anomalies, topological field theory, and string theory. This talk is […]

  • Memorial Conference for the founders of index theory: Atiyah, Bott, Hirzebruch, and Singer

    Virtual

    In 2021, the CMSA hosted a lecture series on the literature of the mathematical sciences. This series highlights significant accomplishments in the intersection between mathematics and the sciences. Speakers include Edward Witten, Lydia Bieri, Simon Donaldson, Michael Freedman, Dan Freed, and many more. Videos of these talks can be found in this Youtube playlist. https://youtu.be/vb_JEhUW9t4 […]

  • Type theory from the perspective of artificial intelligence

    https://youtu.be/79ymkGQW3b4 Speaker: David McAllester - Toyota Technological Institute at Chicago Title: Type theory from the perspective of artificial intelligence Abstract: This talk will discuss dependent type theory from the perspective of artificial intelligence and cognitive science. From an artificial intelligence perspective it will be argued that type theory is central to defining the "game" of mathematics […]