Por Lia Malato (Universidade de Lisboa).

What is the future of mathematics? To explore this question, we will focus on two key goals. The first goal is to present a functional interpretation based on Shoenfield’s functional interpretation in order to translate a typed extension of classical first-order logic into itself. With this functional interpretation it is then possible to state a generalized version of Herbrand’s Theorem and to retrieve its original formulation. The second goal is to introduce the proof assistant Lean by explaining its fundamental mechanisms and to show how Lean can contribute to the development of mathematics. Finally, we will illustrate how the above functional interpretation can be described and formalized in Lean.

Transmissão via Zoom (pw: 919 4789 5133).