What have we built so far? (part 1 of 2)
This is a follow-up to the explanation of our mission statement, which describes what Lurch is aiming to be. It answers the natural next question, “How far are we toward that goal?”
A word processor with mathematical semantics
To judge your mathematical reasoning, Lurch needs to know more than a typical word processor–not just how your document should look, but what your document means.
(This is different than WYSIWYM, where the system needs to understand what you mean in terms of your document structure. Lurch needs to understand what your symbols mean mathematically. If you write a+b, a typesetting system does not care whether it’s adding integers or combining elements of a group, as long as it typesets it nicely. Lurch cares, or it can’t judge your work.)
The ability to store mathematical semantics in a word processing document has been built into Lurch since the beginning.
The green lights follow steps of work Lurch judged correct, red lights incorrect. (In this example, the red light is because the wrong reason was provided.) Yellow lights follow steps that are unjustified, but used later, a.k.a. hypotheses or “givens.”
The beauty of bubbles
The screenshot above may make you ask, “Surely the software is not reading actual English prose, and lifting meanings from it!” Indeed, natural language processing is a hard problem, and Lurch does’t do it. So how does it know which words to pay attention to?
The user indicates each meaningful phrase with a single click or keystroke. It’s as easy to mark something meaningful as it is to apply a format like bold or italic.
In the screenshot below, the user has highlighted a phrase containing mathematics, and the mouse pointer (not shown) is hovering over the red button entitled “Insert meaningful expression.”
The user clicks that button, and the document changes.
The red “bubble” around the phrase indicates that Lurch understands its mathematical meaning. (The “∀ quantification” means that the expression is universally quantified. Other expressions have other labels, such as “+ expression.”)
Like in Word’s equation editor, bubbles are only visible when the user’s cursor is in them. Thus the first screenshot in this post is not cluttered with bubbles, but they’re there.
This paradigm gives the author the ability to write as much exposition between steps of work as they like, even including nonsense (e.g., an example of what not to do), and Lurch will happily ignore it, until the next phrase the author marked as meaningful.
Marking which words are reasons is very similar; the user clicks the blue toolbar button to create a different kind of bubble, one that modifies a red bubble.
The arrow on the reason bubble points to the meaningful expression it modifies. (The red bubble is invisible because the cursor is in the blue one.)
Freedom of Style
So users can write documents however they like, with bubbles as a thin layer of decoration that tells Lurch the author’s intentions. But their writing style is unrestricted; they write proofs as they see fit. To prove it, I end with three screenshots of the same proof, done in three very different styles. Lurch has validated each step in each style; only the mathematics within the style matters to Lurch.