Proof Verification with Lurch
Prof. Ken Monks, University of Scranton
Abstract: Would your students benefit from an easy-to-use, open-source, web-based word processor that could check their assigned mathematical proofs? In this talk we introduce Lurch, our software project designed specifically for this purpose. We will explain how you can use this software and accompanying course materials, and customize it for your own purposes. While existing proof verification tools like Lean, Isabelle, Coq, and Mizar are powerful and effective, they often have steep additional learning curves and can be difficult to customize. We will explain how the custom Lurch validation algorithm overcomes these challenges, and pose some questions for future work.
Tea and refreshments available at 3:00 p.m. in the Assmus Conference Room (CU 212).
