Colloquium and Workshop on
“Mathematical Language and Practical Type Theory”
31 January to 4 February 2020
organized by
Thomas Hales (Pittsburgh), Peter Koepke (Bonn)
Friday, January 31 (Retirement Colloquium for Peter Koepke)
| 15:00 - 16:00 |
Tom Hales The Formalization of Mathematics (abstract, slides) |
| 16:45 - 17:45 | Peter Koepke Life in Logic (slides) |
Saturday, February 1
| 9:15 - 10:15 |
Marcos Cramer Analyzing Mathematical Language Logically and Linguistically: From Naproche to Frames (abstract, slides) |
| 10:45 - 11:45 |
Benedikt Löwe Technology adoption in mathematical research: automated proof-checking as a case study (abstract) |
| 11:45 - 12:45 |
Andrei Paskevich ForTheL, a formal language in human clothes (abstract) |
| 14:30 - 15:30 |
Adrian De Lon, Peter Koepke, Anton Lorenzen Introduction to the Naproche-SAD system (a short tutorial) |
Sunday, February 2
| 9:30 - 10:30 |
Adrian De Lon, Peter Koepke, Anton Lorenzen Parsing ForTheL in the Naproche-SAD system |
| 11:00 - 12:00 |
Sebastian Ullrich Embedding languages into Lean 4 (abstract, slides) |
| 13:00 - 13:30 | Mario Carneiro Lean tutorial on groups |
| 13:30 - 14:00 | Floris van Doorn Tactics in Lean (abstract, slides) |
| 14:00 - 14:30 |
Josef Urban
Informal2Formal: Automatic formalization by statistical and semantic parsing of mathematics (slides, slides with Chad Brown) |
| 14:30 - 15:00 | Kevin Buzzard At the coal face (abstract) |
Monday, February 3
| 9:00 - 10:00 |
Bernhard Schröder
How proofs are told. Linguistic aspects of proof texts (abstract, slides) |
| 10:00 - 10:30 |
Aarne Ranta From Logical to Grammatical Framework (abstract, slides) |
| 11:00 - 12:00 | Aarne Ranta GF-Tutorial |
| 13:30 - 14:00 |
Makarius Wenzel The Isar Proof Language after Two Decades (abstract, slides) |
| 14:00 - 14:30 |
Cesary Kaliszyk, Florian Rabe
Towards an Intuitive Language for Formalizing Mathematics (abstract, slides) |
| 14:30 - 15:00 |
Konstantin Verchinine
How the system SAD was born in Kiev (abstract) |
Tuesday, February 4
| 9:00 - 9:30 |
Bernhard Fisseni, Deniz Sarikaya Frames for mathematical proofs (abstract, slides) |
| 9:30 - 10:00 |
Merlin Carl
Diproche - Automated Proof Checking for Didactical applications (abstract, slides) |
| 10:00 - 10:30 |
Michael Kohlhase Corpus-Based Meta-Mathematics: Flexiformal Mathematics across various Systems and Languages (slides) |