Formalizing mathematics in the proof assistant Agda and extracting algorithms from transfinite proofs

Still even the current generation of theorem provers is very exciting. It's fun to talk the computer into accepting our proofs, and invariably we learn something about our proofs in the process. In this workshop, we'll cover the basics of Agda, one of the well-known proof assistants. The workshop will start as a guided tour. You belong to the target audience iff you have some experience in writing down mathematical proofs, for instance if at some point you proved Gauß's sum formula using induction. Knowledge of Haskell is beneficiary (modulo syntax, Agda is a superset of a subset of Haskell), but not required. If people are still interested and have the energy, we will then also discuss how concrete algorithms can be extracted from proofs involving transfinite methods. Surprisingly, this is possible! By a trick related to "continuation-passing style" in computer science. You don't need to install Agda beforehand, we will use the online version at https://agdapad.quasicoherent.io/. Literature: https://plfa.github.io/ 🧮