NAPROCHE

The Naproche natural proof assistant emulates the usual reading and checking of mathematical proofs which combine natural argumentative language with symbolic material and are often typeset using LaTeX.

Theorem. $$\sqrt{2}$$ is irrational.
Proof. Proof by contradiction. Assume that $$\sqrt{2}$$ is rational. Take natural numbers $$m,n$$ such that $$n\neq 0$$ and $$\frac{m}{n} = \sqrt{2}$$ and if $$m$$ is even then $$n$$ is odd. Then $$\frac{m^2}{n^2} = 2$$ and $$m^2 = 2 \cdot n^2$$. Hence $$m$$ is even and $$n^2 = m \cdot \frac{m}{2}$$. But then $$n$$ is even. Contradiction. Qed.

In the Naproche system natural language parsers are extended to translate mathematical texts into symbolic formulas; thereafter automated theorem provers check whether these formulas can be proved from relevant preceding formulas.

The parsers of the Naproche (Natural Proof Checking) system define an accepted input language ForTheL (Formula Theory Language) which constitutes a controlled natural language (CNL) for mathematics. Various results from undergraduate university mathematics have been formalized in ForTheL and proof-checked by Naproche.

Naproche demonstrates that formal mathematics can be carried out in a language which is immediately readable by mathematicians. Naproche texts may be structured in the familiar declarative proof style. Text can also be input in a LaTeX format for mathematical typesetting.