Lurch: a word processor built on OpenMath that can check mathematical reasoning.
Nathan C. Carter, Kenneth G. Monks · 2013
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.