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, type-theory |
| 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 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
