Talks

Slides of Naproche- and ForTheL-related talks.

2025

• Peter Koepke, Naproche – Talking to ATPs (EuroProofNet School on Natural Formal Mathematics; Bonn, Germany)

• Peter Koepke, A Naproche Teaser (EuroProofNet School on Natural Formal Mathematics; Bonn, Germany)

• Adrian De Lon, Naproche-ZF (EuroProofNet School on Natural Formal Mathematics; Bonn, Germany)

2023

• Marcel Schütz, Foundational libraries in Naproche (CICM; Cambridge, UK)

2020

• Adrian De Lon, Peter Koepke, Anton Felix Lorenzen, ForTheL for Type Theory (AITP; Aussois, France)

• Peter Koepke, A Brief Tutorial on Mathematical Formalizations in Naproche-SAD (HCM Workshop: Mathematical Language and Practical Type Theory; Bonn, Germany)

• Peter Koepke, ForTheL as a Controlled Natural Language for Lean (Methods in Mathematics/Lean Together 2020; Pittsburgh, USA)

2019

• Peter Koepke, An Introduction to Haskell and Naproche-SAD

• Peter Koepke, Making Set Theory Great Again: The Naproche-SAD Project (AITP; Obergurgl, Austria)

• Peter Koepke, Modeling Human Proof Checking in the Naproche-SAD System (ICMS; Edinburgh, UK)

• Peter Koepke, Textbook Mathematics in the Naproche-SAD System (CICM; Prague, Czech Republic)

2018

• Steffen Frerix, Peter Koepke, Automatic Proof-Checking of Ordinary Mathematical Texts (CICM 2018; Hagenberg, Austria)

• Steffen Frerix, Peter Koepke, Making Set Theory Great Again: The Naproche-SAD Project

• Steffen Frerix, Peter Koepke, Revisiting SAD (Part 1), Revisiting SAD (Part 2) (AITP; Aussois, France)

• Steffen Frerix, Peter Koepke, Text-Orientated Formal Mathematics (FLoC 2018, Oxford, UK)

• Peter Koepke, Legible Formal Mathematics based on SAD

2016

• Ioanna M. Dimitriou H, Peter Koepke, Revisiting Paulson's Theory of the Constructible Universe with Isar and Sledgehammer (AITP; Obergurgl, Austria)

• Peter Koepke, Set Theory and Formal Mathematics (Menachem Magidor 70th Birthday Conference; Jerusalem, Israel)

2015

• Peter Koepke, Formalism and Computations (CLMPS; Helsinki, Finland)

• Peter Koepke, Foundations for Formal Mathematics (5th Colloquium of HCM Research Area KL; Bonn, Germany)

• Peter Koepke, Natural Formalism (Philosophy of Mathematics Seminar; Oxford, UK)

2011

• Peter Koepke, Formal Mathematics and Controlled Natural Language (Oberseminar Diskrete Optimierung; Bonn, Germany)

2007

• Andrei Paskevich, The syntax and semantics of the ForTheL language