Session:Formalizing mathematics in the proof assistant Agda

From 36C3 Wiki
Description for students of mathematics, computer science or a related subject
Website(s)
Type Workshop
Kids session No
Keyword(s) science, coding
Tags mathematics, type-theory
Processing assembly Assembly:Curry Club Augsburg
Person organizing Iblech
Language en - English
en - English
Other sessions... ... further results

(Click here to refresh this page.)

Starts at 2019/12/28 21:00
Ends at 2019/12/28 23:00
Duration 120 minutes
Location Room:Seminar room 13

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. After a short intro to the general theory, we'll get to lots of hands-on examples. Bring your laptop and have Agda installed before the workshop starts (Debian package agda, NixOS package haskellPackages.Agda). 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.

Literature: https://plfa.github.io/

Transcript of what we did in the session: https://etherpad.wikimedia.org/p/36c3-agda