Universität Bonn

School on Formal Mathematics

This one-week school teaches practical theorem proving in the three proof assistants with the greatest coverage of (research) Mathematics: Coq, Isabelle and Lean as well as smaller, more specialized systems. Key people from the research groups have indicated their willingness to teach (and supervise practical formalization attempts) in this school, drawing on tutorial material of the various systems. Participants of the school will be asked to work on small formalization projects which eventually could lead to contributions to formalization libraries. There will be a couple of introductory and special lectures.

Guillaume Allais (University of Strathclyde): Agda

Guillaume Allais: A Quick Tour of Agda

Bild © Hausdorff Center for Mathematics / YouTube

Guillaume Allais: Syntaxes for Binding and their Semantics

Bild © Hausdorff Center for Mathematics / YouTube

Steve Awodey (Carnegie Mellon University): What is HoTT?

Steve Awodey: What is HoTT?

Bild © Hausdorff Center for Mathematics / YouTube

Andrej Bauer (University of Ljubljana): Constructive Mathematics - How to not believe in the Law of Excluded Middle

Andrej Bauer: Constructive Mathematics - How to not believe in the Law of Excluded Middle

Bild © Hausdorff Center for Mathematics / YouTube

Mario Carneiro (Carnegie Mellon University): System Introductions I - Lean

Mario Carneiro: System Introductions I - Lean

Bild © Hausdorff Center for Mathematics / YouTube

Mario Carneiro (Carnegie Mellon University): Lessons for Metamath

Mario Carneiro: Lessons for Metamath

Bild © Hausdorff Center for Mathematics / YouTube

Manuel Eberl (Universität Innsbruck): System Introductions II - Isabelle

Manuel Eberl: System Introductions II - Isabelle

Bild © Hausdorff Center for Mathematics / YouTube

Yannick Forster (Centre Inria de Paris): System Introductions I - Coq

Yannick Forster: System Introductions I - Coq

Bild © Hausdorff Center for Mathematics / YouTube

Peter Koepke (University of Bonn): Naproche

 

Peter Koepke: System Introductions II - Naproche

Bild © Hausdorff Center for Mathematics / YouTube

Peter Koepke First-Order Mathematics and Naproche

Bild © Hausdorff Center for Mathematics / YouTube

Michael Kohlhase (FAU Erlangen-Nürnberg): System Introductions II - sTeX/ALeA

Michael Kohlhase: System Introductions II - sTeX/ALeA

Bild © Hausdorff Center for Mathematics / YouTube

Michael Kohlhase (FAU Erlangen-Nürnberg): ALeA - Flexiformal Education

Michael Kohlhase: ALeA - Flexiformal Education

Bild © Hausdorff Center for Mathematics / YouTube

Sam Owre (SRI International): PVS

Sam Owre: System Introductions I - PVS

Bild © Hausdorff Center for Mathematics / YouTube

Sam Owre: Modularity in PVS

Bild © Hausdorff Center for Mathematics / YouTube

Josef Urban (CIIRC - CTU): Theorem Proving and AI

Josef Urban: Theorem Proving and AI

Bild © Hausdorff Center for Mathematics / YouTube

Freek Wiedijk (Radboud University): HOL Light

Freek Wiedijk: System Introductions I - HOL

Bild © Hausdorff Center for Mathematics / YouTube

Freek Wiedijk: More on HOL Light

Bild © Hausdorff Center for Mathematics / YouTube

Freek Wiedijk: Even more on HOL Light

Bild © Hausdorff Center for Mathematics / YouTube

Mario Carneiro (Carnegie Mellon University) and Andrej Bauer (University of Ljubljana): Universes in Set/Type Theory

Mario Carneiro and Andrej Bauer: Universes in Set/Type Theory

Bild © Hausdorff Center for Mathematics / YouTube