Računalniška delavnica: Egbert Rijke, Formalization of mathematics in Agda

Formalization of mathematics in proof assistants is becoming increasingly more popular among research mathematicians and students. It's not hard to see why. For some, proof assistants are a game. The puzzles it is offering are theorems of mathematics. Others use it to learn about mathematical reasoning. The proof assistant gives instant feedback, tells you what next steps have to be proven, it will tell you when a construction is inaccurate, and it will tell you when you have completed your proof. And finally, it should not be underestimated that the large libraries of digitized mathematics that are currently being created by communities of enthusiastic mathematicians and computer science around the world are becoming a useful resource for mathematical researchers and students alike.

In this workshop we will learn how to formalize mathematics in the proof assistant Agda, using the agda-unimath library.

Agda is known for its simplicity, and strong pattern matching algorithms. We will be focussing on formalizing definitions, theorems, and proofs in elementary number theory and combinatorics.

Delavnica bo potekala v angleškem jeziku. Preko Zooma jo lahko spremljate na povezavi https://uni-lj-si.zoom.us/j/98391257025.

PRIJAVE in več informacij o računalniških delavnicah lahko najdete na spletni učilnici.