Lurch [5] is a free word processor that can check the mathematical reasoning in a document, including the steps of a mathematical proof, even one not written in a formal style. This paper covers our goals, implementation in terms of OpenMath, and a brief overview of the underlying validation engine.1
1.1
Lurch is a free word processor that can check the steps of a mathematical proof, and we have
focused the current version on the needs of introduction-to-proof courses, covering topics such
as logic, introductory set theory, and number theory. Lurch is built on OpenMath [
Our user interface guideline is that users should be able to write math in whatever style or notation they prefer, with exposition inserted where they feel it's helpful. Especially in a pedagogical context it is important for the notation and style used in the software to match that of the textbook and lecture notes, so as not to be an obstacle for the student. Of course, pencil and paper won't tell you whether your proof is correct, but Lurch will, in addition to providing the other bene ts that any word processor does, such as cut and paste.
Lurch is for student use. We're targeting students in their rst proof-based courses, where Lurch can give frequent, immediate, clear feedback on the validity of the steps in their proofs. That's the part of the mathematical community we're excited about reaching.
Therefore Lurch is an entirely di erent kind of product than existing proof checkers (e.g.,
Mizar [
1Lurch was supported from 2008-2012 in part by the National Science Foundation's Division of Undergraduate Education, in the Course, Curriculum, and Laboratory Improvement program (grant #0736644). Views expressed in this document are not necessarily those of the National Science Foundation. We want the only learning curve students encounter to come from the mathematics itself, not Lurch.
Existing research on educational technology suggests that our goals make sense and are
achievable. Investigations into the e ects of automated assessment systems (AiM [
This section explains how far we have come towards achieving the goals in Section 1.2.2 For
more details than what this section provides, see [
Consider the screenshot of the Mac version of our application in Figure 1. The red and green thumbs and yellow lights interspersed throughout the document are Lurch's feedback on the correctness of each step of the user's work. (This feedback can be hidden to obtain a clean view for printing.) A green thumbs-up icon follows a correct step of work that is correctly justi ed, a red thumbs-down icon follows a step that contains an error or is supported by the wrong reason, and yellow lights follow mathematical expressions that are used as premises to justify later steps of work, but are not themselves justi ed (e.g., the hypotheses in a proof).
Students can hover their mouse over any of these colored icons for a brief explanation of its meaning, or double-click it for a detailed report. In order to provide this kind of feedback, Lurch needs to know the meaning of the mathematical expressions in the document.
In order for a section of text to be treated as a mathematical expression, the user must mark it as such with a single click of a toolbar button (or the corresponding keyboard shortcut). The user selects a portion of text that he or she wishes Lurch to treat as meaningful mathematics, and then clicks the \Meaningful expression" button on the toolbar. Lurch then wraps the text in a bubble and reports the understood meaning in a tag atop the bubble, as in Figure 2. Lurch draws a bubble around a mathematical expression if and only if the user's cursor is inside it. Both LyX and Word have somewhat similar interfaces for editing mathematics.
The user will create bubbles often, and thus doing so must be intuitive and take nearzero time. The \Meaningful expression" button appears on the Lurch toolbar near formatting options such as bold and italic. It is just as easy to mark text as meaningful as it is to use one of those common formatting commands; a single click or keystroke does it.
This interface enables Lurch to know which portions of the user's document he or she considers meaningful mathematics. Also, in line with our goals from Section 1.2, the user is stylistically free to structure their document their own way. Because meaning is determined by what sections of text have been bubbled, the user can alternate whenever they like between expository text in any natural language and meaningful mathematics, and arrange their work as informal sentences, formal proof structures, or varying levels in between.
This interface also brings a pedagogical bene t. Student users, just learning what a proof is, are forced to indicate what parts of their own proofs are meaningful and which are not. Experience from testing shows us that students come away from a Lurch-integrated course knowing very solidly how a proof is structured, because they had to point out this structure to Lurch before it would check their work.
2At the time of this writing, the current version of Lurch is 0:7992, released on May 9, 2013.
Lurch is not yet at version 1.0, and changes to the current design and interface will come as we evolve our ideas, especially in response to testing. There are many advanced interface features we'd already like to add, including automatic bubbling of statements and reasons, and a visualization of the inference and property graphs. Such features will be able to be enabled or disabled as the user's skills and needs require. 3 3.1
All Lurch documents are stored as OpenMath data structures, from the document level (using
application of symbols for concepts like \paragraph") down to the atomic level (using OpenMath
integers, strings, variables, and so on).3 In order to see how these structures are formed, we
3Although OMDoc [
Lurch makes the following three major categories of bubbles available to users, and provides
toolbar buttons for creating each. The full set of rules stipulating which bubble types can
contain others is given in [
Contexts: Shown using green bubbles, Contexts delimit the scope of declared variables and indicate subproof blocks constructed in the course of writing some kinds of proofs. Properties can be used to modify neighboring MEs, for the purpose of attaching to them labels (like \label in LATEX), reasons (citations of existing rules), and premises (references to earlier statements in the same proof). Although no bubbles are visible in Figure 1 because the cursor is at the end of the document, it contains many invisible ones. For example, on the third line of the proof, the expression 8x; (g f )(x) = g(f (x)) is an ME and the word \composition" on the next line is a reason property that applies to it and the preceding ME. Properties can apply to any number of adjacent, successive MEs, either to the left or right of the property itself. They do not alter the intrinsic meaning of MEs, but only tell Lurch how to work with those MEs (by adding labels, reasons, and so on).
It is possible to see the locations of all bubbles in a document; when a user enables that option, Lurch shows bubble boundaries as in Figure 3. For even more information, a user can direct Lurch to include the contents of each bubble's tag after its latter boundary. This results in a very cluttered view, but it is one way to see full information quickly.
An ME which is not contained inside any other ME is called a top-level ME. A Lurch document can be thought of as a sequence of top-level MEs M1; : : : ; Mn. Although there is normally text between the Mi, Lurch ignores it for the purposes of validation and giving the user feedback. Properties assign attributes to these MEs and Contexts group together collections of MEs that have a common purpose or relevance.
Lurch documents also depend on other Lurch documents in the same way that one chapter of a math book might depend on a previous chapter. The rules cited in Figures 1 and 3 are available because their de nitions appear in a document on which that one depends. In Lurch, an imported document acts as if it appears, invisibly and in a read-only state, in its entirety, at the top of the document that imports it. 3.2
Every ME is either a simple ME (containing no other MEs), of type integer, real, variable,
constant, string, operator, or quanti er; or a compound ME (containing other MEs), of type
function application or quanti cation. These correspond roughly to the major types of simple
and compound expressions in OpenMath [
Lurch infers the meaning of a simple ME from the text in its bubble. Thus a simple ME might contain the text 42, and be interpreted as an integer, or contain 3.14159 and be interpreted as real. Similarly, x would be a variable, "Life, the Universe and Everything" hierarchies.
[ [ ] [
Because most users would rather type the expression in a more standard notation, Lurch tests the contents of every simple ME bubble to see if those contents can be understood by a built-in parser. If so, then that ME bubble is treated as the (possibly compound) ME determined by the parsing, while still appearing as a single bubble in the document. This allows a compound ME to be entered with the same ease as a simple ME and usually produces more legible results. For example, 3 f (x + 1) can be entered in the typical calculator notation 3*f(x+1), or 3 f(x+1). Such MEs have the same meaning as the fully \expanded" version shown above.
Users can expand and collapse MEs between these two forms by using the context menu on the ME bubble itself. The parser is a convenience feature that allows users to enter compound MEs in a natural notation, but in every case the actual meaning of an ME is its expanded form, which is indicative of how it is stored as underlying OpenMath data.
Eventually the language that Lurch parses will be customizable, but the current version just uses a standard mathematical syntax. Here are some example expressions the parser currently understands.
x^2-1=(x-1) (x+1)
3^2>2^3 8x, x2A\B , x2A and x2B f x : x2=x g Lurch has a symbol toolbar so that users can click to enter symbols like 8 and 2=; this is the bottom toolbar in Figure 1, with each symbol a button that opens a palette of related symbols. The software also automatically replaces common LATEX codes for such symbols with the symbols themselves, so users who prefer keyboard shortcuts can learn those codes.
Although the internal storage for these well-known symbols uses standard OpenMath symbols such as subset from content dictionary set1, that may need to change because the meaning of the symbol in Lurch is whatever the user gives it by means of de ned rules, which may or may not match the meaning in the content dictionary.
The current version of Lurch does not have mathematical typesetting capabilities, but later versions will include them. In particular, superscripts, subscripts, and fractions must be input using calculator-like shortcuts, such as x^2. But our current focus is on introduction to proof courses, and so Lurch comes with topics such as logic, set theory, and number theory, which don't really need much more than this plain notation (with a healthy supply of mathematical symbols). 4
The raison d'^etre of Lurch is validation of student work. For each step of student work, Lurch
should give feedback about the correctness of that step. In most cases, an ME is a step of work
if and only if it is a top-level ME and the user has attached a reason to it; details can be found
in the Lurch Advanced Users' Guide [
A constant declaration or variable declaration will get a green validation icon if the following conditions are met.
1. It is not already declared, i.e., it is not in the scope of the declaration of the same identi er either as a variable or a constant.
2. It does not have a reason assigned to it.
If either of these conditions are not satis ed, the validation icon for the rule will be red and double clicking or hovering over it with the mouse will give a message indicating which of the conditions was not met, and how you might go about xing it.
4The Advanced Users' Guide is a speci cation of a system, with no attention given to the motivations behind the design. Lurch is not yet at version 1.0, so the design is not set in stone, and thus a motivating document is not yet written.
Such a speci cation exists for each type of ME in Lurch, but the nontrivial ones are too complex to list here. Instead we illustrate the algorithm with an example.
All of the rules and de nitions that are available to students when doing their assignments in Lurch are written in Lurch documents directly. Users who want to customize the mathematics in Lurch can inspect those built-in, foundational documents, copy them, and alter them to suit their own style, or write new ones from scratch. As mentioned above, a document containing rule de nitions can be included in another document as a dependency, making the rules in the former available in the latter.
The libraries that ship with Lurch de ne rules that are based on the natural deduction style of proof used in the second author's introduction to proof course. However there is no need to use these rules at all. An instructor can type his or her de nitions, rules, and theorems directly into Lurch to make new dependency documents that the students can then use when working on their assignments.
For example, Figure 4 shows a snippet of lecture notes that an instructor might type into a Lurch document to de ne a new rule. He rst declares a new term (increasing, bubbled as a constant declaration) which Lurch veri es is not already de ned. He then speci es his proposed de nition in the form and with the level of detail and speci city that he desired. The more advanced bubble structure that the instructor must use to alert Lurch to this rule's structure appears in Figure 5, using visible bubble boundaries as introduced in Figure 3.
Finally, when a student uses the rule to justify a statement, he or she does so by supplying the two required premises, and justi es the expression g(s) < g(t) by citing as a reason the name of the rule (\increasing" in this case), as in Figure 6. Lurch checks that for the appropriate values of f , s, and t in the rule de nition, the required premises are available to justify the desired conclusion.
In addition to the syntactically de ned rules Lurch currently supports, we would also like to add rules validated by a built-in computer algebra system. Doing so would enable us to support typical algebra or calculus topics as naturally as we currently support proof-related ones.
This paper does not include all the details of the validation algorithm, but interested readers
can inspect [
In other words, the results of validation at point P never change the results of validation
at some earlier point Q, and therefore Lurch can validate a document quickly, not having to
read it more than once. Although mathematicians sometimes write documents for which this
strict ordering of ideas and reasons fails to hold, Velleman [
The proof of such a theorem involves showing that the speci cation for each type of meaningful expression depends in no way on the results of validation of meaningful expressions later in the document. The e ciency bene ts of this theorem have not yet been integrated into Lurch, because both the design and implementation are still maturing. 5
Lurch was tested throughout an introduction to formal logic class the rst author taught at
Bentley University in the fall of 2008, and an introduction to proofs course for mathematics and
mathematics education majors the second author taught at the University of Scranton in the
spring of 2013. In both cases, student response was very positive, the details of which appear
in [
Lurch has many opportunities for improvement, including testing in courses not taught by the developers and new features (typeset mathematics, more e cient validation algorithms, more attractive visual representations of premise relationships, and an even less obtrusive bubbling interface). But the current version, despite its opportunities to improve in many ways, shows all the signs of having been very bene cial in the courses in which it has been used.
The Lurch team invites additional collaborators for writing new mathematical topics in Lurch, doing further classroom testing, and software development.