Writing "Semi-Formal" Proofs

The question becomes interesting when it is interpreted as a technical question about the extent to which we can have a semi-formal language somehow in-between the truly formal proofs, which are largely unreadable by humans, and the informal proofs used by professional mathematicians.

In fact, there has been some truly interesting work on this topic. In particular, the Naproche proof system implements this semi-formal language idea. See also this article describing the system and try out the web interface examples).

The idea of Naproche (for Natural language Proof Checking) is to focus precisely on the layer of proof detail that exists between the fully formal proofs that can be checked by computer and the fully natural language proofs used by humans. When using Naproche, one creates proofs in a controlled natural language, a semi-formal natural-seeming language, while under the hood the system converts the semi-formal proof to an unseen fully formal proof, which is proof-checked by one of the standard formal proof-checkers.

The effect is that by using the semi-formal language, one guides Naproche to a formal proof which can then be verified. Thus, one gains the value of the verified formal proof, without needing ever to explicitly consider the formal proof object.

Furthermore, because the syntax of the controlled natural language uses TeX formalisms, the semi-formal proofs and theorem can be automatically typeset in an appealing way.

I encourage everyone to go try out the web interface examples, which includes Naproche semi-formal (but fully verified) proofs of elementary results in group theory, set theory, and a chunk of Landau's text.

Here is an example of Naproche text, and you may also consult the pdf output here. This text entered verbatim results in the formal proof object, which is verified as correct. (The pdf and proof object are temporary files, but can be generated by clicking on "create pdf" or "Logical check" at the web interface.)

Axiom. 
There is no $y$ such that $y \in \emptyset$.

Axiom.
For all $x$ it is not the case that $x \in x$.

Define $x$ to be transitive if and only if 
for all $u$, $v$, if $u \in v$ and $v \in x$ 
then $u\in x$. Define $x$ to be an ordinal 
if and only if $x$ is transitive and for all 
$y$, if $y \in x$ then $y$ is transitive.


Theorem.
$\emptyset$ is an ordinal.

Proof.
Consider $u \in v$ and $v \in \emptyset$. 
Then there is an $x$ such that $x \in \emptyset$. 
Contradiction. Thus $\emptyset$ is transitive.
Consider $y \in \emptyset$. Then there is an 
$x$ such that $x \in \emptyset$. Contradiction.
Thus for all $y$, if $y \in \emptyset$ then $y$ 
is transitive. Hence $\emptyset$ is an ordinal.
Qed.

Theorem.
For all $x$, $y$, if $x \in y$ and $y$ is an 
ordinal then $x$ is an ordinal.

Proof.
Suppose $x \in y$ and $y$ is an ordinal. Then 
for all $v$, if $v \in y$ then $v$ is transitive. 
Hence $x$ is transitive. Assume that $u \in x$. 
Then $u \in y$, i.e. $u$ is transitive. Thus $x$ 
is an ordinal.
Qed.

Theorem: There is no $x$ such that for all $u$, 
$u \in x$ iff $u$ is an ordinal.

Proof.
Assume for a contradiction that there is an $x$ 
such that for all $u$, $u \in x$ iff $u$ is an ordinal.
Lemma: $x$ is an ordinal.
Proof:
Let $u \in v$ and $v \in x$. Then $v$ is an ordinal, 
i.e. $u$ is an ordinal, i.e. $u \in x$. Thus $x$ is 
transitive. Let $v \in x$. Then $v$ is an ordinal, 
i.e. $v$ is transitive. Thus $x$ is an ordinal. Qed.

Then $x \in x$. Contradiction. Qed.

A "proof" is really a meme, an organism constituted not of cells but of thoughts. It lives in peoples heads, sometimes mutates, and often (unfortunately) dies. In colonies, they tend to live longer and reproduce more effectively. The ``proof'' that we write down is the sex organ of these mathematical memes: it's only purpose is to facilitate reproduction from the author's head into yours.

Now your head is different from mine, and both our heads are different from Milnor's. It is completely appropriate (and even expected) that the reproductive needs are different in these different circumstances. It's not a matter of finding the "right" level of detail, just a matter of serving different purposes. Ultimately, you will know what your brain needs better than anyone else, and just like the rest of us you will have to work to fix what you read into what you need.

Perhaps this item is relevant:

Thomas Hales, Formal Proof, Notices of the AMS 55 Issue 11 (2008) pp 1370-1380. (pdf)

And another item: Lamport's "structured proofs":

Leslie Lamport, How to write a proof (1995) (abstract)