Session:Formalizing mathematics in the proof assistant Agda
Description  for students of mathematics, computer science or a related subject 

Website(s)  
Type  Workshop 
Kids session  No 
Keyword(s)  science, coding 
Tags  mathematics, typetheory 
Processing assembly  Assembly:Curry Club Augsburg 
Person organizing  Iblech 
Language  en  English 
Other sessions...

(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 wellknown proof assistants. After a short intro to the general theory, we'll get to lots of handson 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/36c3agda