# 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.