Lurch Tutorial Session

Tutorial Schedule

The workshop schedule is online here.

What is Lurch?

Lurch is a web-based word processor that can check mathematical reasoning. What differentiates it from well-known and powerful proof checkers like Lean, Coq, and others, is that its purpose is not to support large-scale proof verification, but instead to focus on students in their first proof-based course. It must therefore have an interface that is far more welcoming to students than a standard proof checker has; it must look like ordinary mathematical notation, but with the added benefit that the reasoning can be validated. Students should get real-time feedback on their mathematical reasoning, with the ultimate goal being to improve the learning experience for their first exposure to pure mathematics. A screenshot appears at the end of this page, and can serve as an example of these ideas.

Goals of the Session

We assume no familiarity with the software, and will cover:

• the goals of the project
• the user interface for students
• the user interface for instructors
• the deductive engine on which the software relies

Attendees will complete the workshop with enough knowledge to do both of the following:

• use the software, as a student, to prove basic mathematical facts,
• create materials, as an instructor, for use in a future course, and then use Lurch in that course as a beta tester of the new release
• optionally contribute new code to the GitHub repository, to add new features to the software, if they desire to do so

Contents of the Session

This tutorial session will introduce new users to the latest release of the software Lurch. Although Lurch's first release was in 2008, and that release was reported on at CICM 2013 (1, 2), the software has been rewritten since then and is significantly different (e.g., now running in a web browser.) You can find more details on the latest release below, or view the workshop schedule here.

The new version has been alpha tested in an introduction to proofs course in Spring 2024 and the first official release of that new version can be found on our project website. The new release is drastically different from the old in usability, speed, and reliability.

Where can I try Lurch online?

You can try the current version of Lurch online here, and find an introductory tutorial online here. Throuhgout the remainder of 2024, the software's documentation and its tutorial will grow further.

The screenshot below shows an example proof done in the current version of Lurch, which you can try online. In the screenshot, Lurch has placed green checkmarks to indicate that each of the user’s steps of reasoning are correct. (The cited theorems and the assumption that the variables are integers are not included in the screenshot, for brevity.)

Things to note in the example above:

• the standard notation supported by the user interface
• the focus on the size and style of proofs one covers in an introduction to proofs course
• the informal style, much more flexible than a typical system of formalized mathematics

Organizers

• Nathan Carter, Bentley University, Waltham, Massachusetts, USA
• Kenneth Monks, University of Scranton, Scranton, Pennsylvania, USA