Formalizing mathematics in the proof assistant Agda

From 35C3 Wiki

Revision as of 13:28, 30 December 2018 by Iblech (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Description For students of mathematics, computer science or a related subject.
Website(s)
Type Hands-On
Kids session No
Keyword(s) software, coding, security, science
Tags mathematics
Processing assembly Assembly:Curry Club Augsburg
Person organizing Iblech
Language de - German, en - English
de - German, en - English
Other sessions... ... further results

(Click here to refresh this page.)

Starts at 2018/12/30 11:00
Ends at 2018/12/30 12:30
Duration 90 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/

What we did in the session: https://etherpad.wikimedia.org/p/agda-is-fun