Some day, computers will help working mathematicians of all disciplines in finding and checking proofs. It will feel easy, effortless and natural. Computers might even surpass us, creating a new exciting niche for mathematicians: understanding the mathematical advances put forward by computers. The univalent foundations program by the late Vladimir Voevodsky was an important step towards this vision. However, we aren't there yet.
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.
You don't need to install Agda beforehand, we will use the online version at https://agdapad.quasicoherent.io/.
Literature: https://plfa.github.io/
Note to other people planning self-organized sessions: We don't actually need the full size of Saal D. A room with about 20 seats is sufficient. On Day 0, we will scout the building for alternative options.
Here is a list of more sessions by our group.
🧮