Naproche

Naproche is a natural proof assistant that models the usual reading and checking of mathematical proofs by mathematicians. The naturality of Naproche is twofold: it uses a controlled natural language as its input language, but it also aims for proofs free from clutter and tedious details, i.e., proofs that read naturally to mathematicians. The input language of Naproche is embedded into LaTeX, allowing users to combine natural argumentative language with symbolic material in a manner that is familiar to mathematicians.

Here’s an example of a theorem and proof in Naproche:

Theorem (Cantor). Let $M$ be a set. No function on $M$ surjects onto the powerset of $M$.

Proof by contradiction. Consider a surjective function $f$ from $M$ to the powerset of $M$. Define $$N=\{x\in M|x\notin f\left(x\right)\}\text{.}$$ Thus $N$ is a subset of $M$. Consider an element $z$ of $M$ such that $f\left(z\right)=N$. Then $$z\in N\text{iff}z\notin f\left(z\right)=N\text{.}$$ Contradiction. Qed.

Naproche translates natural language to a formula-based representation and generates proof obligations associated with each step in a proof. Each obligation consists of a conjecture together with hypotheses representing previous facts and local assumptions. Thereafter Naproche uses automated theorem provers to check whether the conjecture of each obligation can be proved from its hypotheses.

Students have successfully formalized a variety of undergraduate mathematics in 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.