The word processor that can check your math


Answers to Questions, Technical Support, and Additional Documentation

General questions

Okay, it's a funny name. The project got that nickname a long time ago, and it stuck. Funny or not, the name has some positive connotations that we hope our project grows to deserve as it matures. For example, a lurch is a big, unexpected step forward. Although the association with the famous butler of The Addams Family is not intended, it is also not unwelcome. That character shares several important qualities with our software:
  • Both are powerful.
  • Both live to serve you.
  • Both are capable of being very formal.
But here's the long story... In 1997, Nathan and Ken began envisioning the Lurch project, but did not have a name for it at that time. Having intimate knowledge of both the mathematical software Maple and the text-based email client Pine, we felt it important to use a tree name. The first thing that came to mind was Oak, but we found out there was already mathematical software by that name (!), although I can't seem to find a link now to that project from more than a decade ago. Taking this as evidence that we were on the right path, we chose another tree, the Larch. This had the positive karma of being the subject of a Monty Python bit. But in 1997, we weren't ready to build "Larch" quite yet, but we did work on a prototype. We called it "Lurch" because it was very like the Larch we envisioned building one day, but it was actually just an initial stumbling step. The prototype was completed in 1999 as part of Nathan's undergraduate work, mentored by Ken. Then a decade passed, a decade in which we would often think about or refer to the project. But Nathan was off getting his Ph.D. and getting married and things like that, so the project was on the back burner. By the time we resurrected it in the 2006-2008 timeframe, we'd been calling it Lurch for about ten years, and couldn't think of calling it anything else.
Sometimes.  There are several things that make this less annoying than it sounds.
  1. Lurch will have a growing number of "shortcut rules" over time.  For example, imagine a rule called "algebra," which would just check to see if an equation you typed was true, according to a built-in computer algebra system.  Lurch already has such a rule, alleviating many steps of tedious proving about basic algebra (and arithmetic, trigonometry, calculus, etc.).  Such a rule can be enabled and disabled for different documents.  Lurch will gain more rules like this one over time (e.g., one for skipping propositional logic proofs).
  2. Users are always free to skip steps in a proof.  The missing steps cannot be validated by Lurch, but if the user is confident that they are correct, they can continue the proof after the skipped step, and ignore Lurch's red mark at the gap.
  3. Instructors who do a good job of choosing axioms, rules, and theorems to support the proofs the students need to do can minimize this problem.  Consider this algorithm, as an instructor:  Write out the proofs you expect your students to do, and look at all the reasons you cited.  Make each one into a theorem or axiom, and provide those to your students.
Yes. Documentation is available online in pdf format here

Those documents and a hands-on tutorial are also available by pressing F1 inside the Lurch application itself. (If you are a developer or thinking about becoming one, you can find the documentation for the Lurch source code itself here.)

The current version of Lurch has most but not all of what we hope to have in Lurch version 1.0 some day.  The current version is fully functional for actually checking mathematics, and reasonably polished for certain applications like propositional logic, predicate logic, elementary set theory, etc.  But there are some major features that are currently missing that we hope to add in future versions.
  1. Mathematical typesetting. The current version cannot display math expressions that are anything other than a horizontal sequence of math symbols and characters.  In particular, it cannot render complicated expressions that contain fractions (like the LaTeX \frac{1}{2}), matrices, etc.  This is naturally a high priority to add in the future.
  2. Customizable parser. While the rules in the current version are completely customizable, the parser that is used to interpret math expressions typed in meaningful expression bubbles (see the Advanced Users Guide) is currently built-in and difficult to extend to new notation.  In the future the parser will be completely customizable by the Lurch author who can make the notation match his or her textbook, lecture notes, or any other notation they invent and would like to use.
  3. Expression types. The rule identifiers that appear in a Lurch rule definition can currently be instantiated with (almost) any expression when trying to determine if the expression being justified and its premises satisfy the rule.  In the future we hope to allow the rule author the ability to restrict rule identifiers so that they can only be instantiated with an expression of a certain type (like a statement, or a set, or a natural number, etc.).  The type of an expression will also be customizable and compatible with the customizable parser.
  4. Higher Level Rules. Currently the if-then and iff rule definitions make it possible to easily write custom rules that can check a single step of your work.  But there are times when the need to validate every step of your work may result in an overly pedantic or detailed proof that focusses on steps that might detract from the main ideas of your proof.  To assist with that we can implement higher level rules as additional rule definition types. Examples of such rules in the current version are the CAS rules which use a CAS to validate any step of work that involves showing two standard CAS math expressions are algebraically equivalent.  In the future we would like to add other such rules, such as a rule that avoids the need to do propositional logic steps individually by having a single rule that checks if the conclusion follow from the premises as a tautology.
  5. Improved AI.  Currently Lurch has a few shortcuts for reducing the burden on the user to bubble things in his proof.  For example, the meaningful expressions on a numbered list are automatically labeled by the line number so that the user doesn't have to label those meaningful expressions in order to refer to them as premises.  It is also assumed that premises that are not cited are automatically cited to be the expressions of the appropriate type immediately preceding the expression being justified.  These shortcuts can be supplemented with additional rules, such as having Lurch find premises wherever they may occur in the document, or having it auto-bubble reasons and labels and premises whenever it can make a reasonable guess in order to save the user work.  Better control over how aggressive Lurch is at doing these things will allow the instructor to decide how much help is too much and how much is just enough.
These are just some of the main features we hope to have in future version.

Technical Support

This question applies only to Lurch 0.75.  In Lurch 0.76, improvements were made to make this confusing situation far less likely, if not impossible. When you run Lurch for the first time after a clean installation the Introductory Dialog that comes up may offer to modify your search paths.  If you do not accept this offer, or if your search paths change after installation as a result of moving the Lurch installation, renaming folders, etc., you can easily repair your search paths. Just click on Help>Show introductory dialog and if it offers to modify your search paths at the bottom of the Introductory dialog, be sure to click on the link that allows it to do so.

Here is an example of the Introductory dialog offering to repair broken or missing search paths (shown on Mac OSX).  Click the link at the bottom to allow it to add those search paths so it can find the Topics and Dependencies it needs.

The Introductory dialog offers to reset broken search paths.

Note that after you click on the link at the bottom you have to completely close and restart the Lurch application (File>Exit) for the paths to take effect.
This question applies only to Lurch 0.75.  In Lurch 0.76, some improvements were made to make this confusing situation far less likely, if not impossible. This can happen if your current document does not have the correct dependency.  Loading any topic from the File>Choose topic menu should fix that problem.  (If you want to start your own topic from scratch with a blank document, choose the Meaningful Documents topic.)  Lurch remembers the last topic you had open the next time you launch the program, so doing this once should fix the problem in the future.  If you do not have any topics to choose from see this FAQ.
Lurch currently requires the DejaVu Sans font in order to render the full set of built-in math symbols.  While it is possible to change the default font for Lurch documents, doing so might cause some math symbols to be missing or display incorrectly. Also changing any math symbols to a font other than DejaVu Sans may cause similar problems.
This question applies only to Lurch 0.75.  In Lurch 0.76, some blackboard bold symbols appear in their own palette in the math toolbar. You can type ℕ, ℚ, ℝ, ℤ and ℂ (or any other blackboard bold character) in Lurch by typing ordinary letters like N, Q, R, Z, and C and then changing their font to jsMath-msbm10. If you want to put blackboard bold characters inside a meaningful expression, you should turn off auto-formatting of the contents of the meaningful expression bubble contents first.  To do this first create your meaningful expression and its contents, then right click on the bubble and choose Stop auto-formatting from the context menu.  Then you can change characters in your math expression to blackboard bold as described above.

Keep in mind that Lurch does not consider character formatting when determining meaning, so that e.g. the expressions ℕ and N will mean the same thing (assuming you made the ℕ by formatting N with the jsMath-msbm10 font).
The answer to this question is simple: they are all just kinds of Lurch documents.  Here are the distinctions.

Lurch document:Starting with just a plain ordinary blank Lurch document, you can type your content, define your own rules, constants, and styles, and save that as your own document like you would do in any other word processor.

Lurch dependency document: Any Lurch document that is saved in the Lurch Search Paths (which are set in the Preferences menu dialog) can be added to another document as a dependency. Any rules, constants, or styles that are defined in a dependency become available in any Lurch document that depends on it.  To add a document as a dependency of your current document, use the File>Document Properties menu.

Lurch Topic Document: Any lurch document can also be marked as being a Topic using the File>Document Properties>Attributes menu. When you save a file marked as such in your Search Paths and restart Lurch, it will show up on your list of topics when you choose the File>Choose topic... menu. When you select a topic from the File>Choose topic... Lurch opens that topic document for you, but clears the document filename so that File>Save will prompt you for a new filename. Thus, selecting a topic gives you a copy of the topic document for you to modify or use without overwriting the original topic file when you save.

Note that you can store any content you like in a Lurch Topic Document. If you want the topic to just provide a blank document with a certain set of rules, constants, and styles available, you can just make an empty Lurch document with the correct dependencies, and then save that as a topic. In the current release the topics categorized as Logic, Number Theory, and Set Theory are of this type.

On the other hand, you can also save word processing content in the topic document to act as a template, or examples, or helpful documentation for that topic. In the current release the topics listed under Problem Sets and Puzzles and the Russell's topic are of this type.

Complicating this further is that we have...

Lurch Topic Associated Help Documents: Each topic document can have associated with it yet another Lurch document that is the help file for that topic. When the topic document is opened, there is a menu option on the Lurch Help menu that says "Start writing help for this document" that allows you or the document author to write an associated help file. Once a topic has such a help file written, anyone using that topic will have a new menu item on the Lurch Help menu that says Help on <name of topic here> that the user can select to read the associated help file for the given topic.

For this release of Lurch, we pointed most of the topic help files to the main dependency that defines the rules loaded in that topic, or gave them no help at all when they are self-documenting by virtue of them containing expository content (e.g. Mini-Set Theory Puzzle or Russell's).

And if this cornucopia of Lurch document types wasn't enough we also have:

Lurch Help Documents: These are currently defined to be files that are opened via a hyperlink, such as those you get when you click on NEXT/PREV links in the Tutorials, or those that you get from the Introductory dialog or from the Help Menu. Like Topics, these also open with the file name cleared for the document, so that if you modify them and try to save them, you will be prompted for a new filename and not accidentally overwrite the original help files.

So Lurch has no shortage of document types or ways to provide help for a given document.

Tips and Tricks

When typing math expressions such as $$x=\cos(t)\Rightarrow \vert x\vert \leq 1$$ it is traditional to italicize the variables like \(x\) and \(t\), but not the function name \(\cos\), the integer \(1\) or the other math symbols. Lurch automatically formats such expressions this way when you wrap the expression in a a meaningful expression bubble (highlight it and press CTRL+[).  You can take advantage of this auto-formatting even for math expressions that are in commentary by temporarily wrapping them in a meaningful expression bubble, and then destroying the bubble (highlight the expression, press CTRL+[ and then CTRL+SHIFT+backspace).  This can save you a lot of typing when trying to italicize just the identifiers that aren't functions in an expression in commentary.
Note that if you don't want Lurch to auto-format the contents of a meaningful expression bubble, you can turn off auto-formatting for that bubble by right clicking on the bubble and choosing Stop auto-formatting from the context menu.  This is useful if you want to override the default formatting of a meaningful expression.
You can set paragraph margins, paragraph alignment, font face, font style, and font size individually for a paragraph or selection, but it can be tedious to set these values repeatedly in order to make section headings, theorems, display math expressions, examples, etc. have a consistent look throughout your document.  To avoid that you can define named styles in Lurch that store one or more of the above five formatting settings so that the entire collection can be applied to a paragraph or selection easily in the future.
To do so simply create an example of the style you want to define in your document, and then with your cursor in the sample, use the Format>Manage formats menu to open a dialog that lets you define a named formatting style based on your current cursor position.  After that you can apply that formatting style to a paragraph or selection by pressing CTRL+SHIFT+F and choosing the style from the list. Pressing CTRL+ALT+SHIFT+F applies the last style you selected, which is helpful when you have to apply the same style to many different selections or paragraphs.
Note that applying a named style in Lurch only applies the attributes of that style to the selection or paragraph.  It does not store the name of the style itself, so that if you redefine the style later on it will not affect the formatting of sections of the document to which that style was previously applied.  A collection of styles can be saved as a Lurch document in your Lurch search path (see File>Preferences to manage and identify search paths) and then used as a dependency to act as a style sheet for your documents.  Lurch comes with several such Stylesheet documents that you can add to your own as a dependency (see File>Document Properties to manage your dependencies).
If you want a fast way to bubble something there is one hotkey you should learn: CTRL+ENTER (use COMMAND in place of CTRL in all hotkeys on a Mac). If you press this without selecting any text it opens a selection menu showing the kinds of bubbles it can insert (unless you are inside an existing bubble in which case it will show you the kinds of bubbles you can change the current bubble to). If you select some text and then press this hotkey you can wrap the selection in whatever type of bubble you like. This latter version also works inside of other bubbles. In particular, inside of rule definitions it allows you to quickly and easily bubble selections as rule conclusions, premises, assumptions, etc.
In addition, there are even faster ways to enter bubbles directly if you know what kind of bubble you want and don't want to wade through the CTRL+ENTER popup menu.
CTRL+[ = insert a generic ME bubble

CTRL+< = insert a label bubble pointing left
CTRL+> = insert a label bubble pointing right
CTRL+; = insert a reason bubble pointing left
CTRL+' = insert a reason bubble pointing right
CTRL+: = insert a premise bubble pointing left
CTRL+" = insert a premise bubble pointing right
If you look at the keyboard, the hotkeys for the property bubbles are laid out like something like this:
  : " (premise left/right)
  ; ' (reason left/right)
< >   (label left/right)
which is sort of natural and easy to remember because they are all in a cluster geometrically on the keyboard and left and right property directions correspond to the left and right key in the pair. Furthermore, if you want to increment or decrement the arrow number on a property bubble after you create it, press the left/right hotkey for that bubble type with your cursor inside the bubble.

Known Bugs

This problem seems to only occur when you have a paragraph with justified alignment, and even then only sometimes.  It is not a bug in Lurch, but rather a bug in the editor widget that Lurch uses as the basis for its word processor.  The cursor seems to stop as you move it to the right side of the screen with the right arrow key, but in reality it continues to move through the letters in your document.  You can usually fix it by temporarily changing the paragraph alignment to left-justified with CTRL+L.
This is is a known bug that only seems to occur in documents that have one or more paragraphs with justified paragraph alignment.  Changing all of the justified paragraphs to be left justified should give you a clean printout.  Also changing the zoom level slightly before printing can sometimes clear up the problem in a small document.

(More information is posted here all of the time.)