Lurch lets you enter math in a document -- and check it, too

Lurch is an open source math word processor which allows you to create documents, insert a full mathematical argument, and validate it, too.

This isn’t just a matter of checking that "2+2=4", either. The program also supports and "understands" algebra, calculus and proofs.

While this sounds complex, Lurch works at many different levels. And at its simplest, you can use the program as basic editor with OpenMath-based support for equations. Create a text document, and enter math expressions using the toolbar, calculator or TeX notation.

Whatever you create is immediately rendered using MathJax, the same display engine used to display equations in just about every browser. And Lurch can save your work as an HTML page, or just a fragment of HTML code, ready for sharing with others.

The program isn’t just about static text entry, though. Simple markup tools allow you to tell Lurch what different parts of the document mean. In the example expression "Since 1<2 and 2<3 we know that 1<3 by transitivity", you would mark up "1<2", "2<3" and "1<3" as meaningful, "transitivity" as the reason, and click "Validate" to have the program check your work.

Better still, the logic behind all this isn’t buried in the source code. Lurch validates your arguments using more than 100 predefined rules, covering everything from "addition" and "multiplication" to "logic", "DeMorgan" and "Cartesian product". These are all ready to view (Meaning > List all defined rules), and you can even add new rules of your own, as necessary.

Lurch isn’t for math beginners. You have to construct an argument before the program can validate it. But if that’s no problem, the rest of the program works very well indeed: it’s simple to use, gives you plenty of freedom in defining your proof, and can easily be extended with custom validation rules.