What is our mission statement trying to say?
When you get bogged down in the details of a project, you check your direction against the beacon of your mission statement. A mission statement should be short and to the point, but may thus leave you wanting more detail. This post fills in details in our own mission statement, which comes in two parts.
Lurch should be as indistinguishable from the ordinary activities of mathematics as possible, except for the additional services it provides. That is, it should only add to your math experience, not change your math experience.
This is our user interface guideline. People write math in their style, a notation they’ve learned, with exposition where they feel it’s helpful. This is true on chalkboard, paper, or LaTeX. So the Lurch user experience must be as similar to those activities as possible. Except, of course, that pencil and paper won’t tell you whether your proof is correct, but Lurch will.
When designing our user interface, if choice A seems more like typical mathematics than choice B, we choose A. There is always room for improvement in this area; we always have ideas that we haven’t yet built. Even so, what we have now is pretty natural.
But that’s for another post…for now, let’s see part 2 of the mission statement.
Lurch should provide the software infrastructure the mathematical community needs for validating rigorous mathematics. That is, it should validate mathematical content created by you — a “spell-checker” for mathematical rigor.
Admittedly, this could be clearer–there already are impressive pieces of software (e.g., Mizar) that validate rigorous mathematics. But proof checkers like Mizar are different from Lurch in these ways:
- They make you learn a specific language and rules. (Lurch lets you define the rules–and eventually the language, but not yet.)
- They automate some proof steps. (Lurch expects you to do the work, and it checks it. Lurch doesn’t help you prove, but helps you learn to prove.)
- Their user interface is for advanced users. Their audience is comfortable with shell scripts and batch files. (Lurch is for the classroom, a word processor with feedback shown visually in the document. See “User Interface,” above.)
We want Lurch to help students learn to prove, and existing proof-checking software serves a technical user with different needs. We’re targeting students in their first proof-based courses, giving frequent, immediate, clear feedback on the steps in their work. That’s the part of the mathematical community we’re excited about reaching.
Now you know what our mission statement says. In a future post, I’ll talk about how close we are to that goal, what we’re lacking, and how to help!