## Writing “Semi-Formal” Proofs

I am very interested in proofs. I have taken an undergraduate course called "Logic and Set Theory" which I found very interesting, but ultimately unsatisfying. My biggest disappointment has to do with the language in which proofs are expressed. It seems to me that we have all of the symbols necessary to express a proof in "pure math". By which I mean, only using symbols and a few specialized words (iff, let, ...). And yet most proofs that I have seen are just walls of English text, interpolated with mathematical symbols.

When I read a complex proof, I find myself needing to transcribe it into pure symbols before I have any chance at understanding it. I have talked to a professor about this, and he informed me that my "pure math" proofs were actually considered informal, and not proper proofs at all! He seemed skeptical that anyone would actually prefer symbols to English.

I have searched Wikipedia and Google for more information, and I see that there is something called a "Formal Proof" (although I have heard this term used in other situations, and so I am not quite sure it means what I think it means) which uses a computer to verify a proof written in a special programing language. As fascinating as that is, it seems to be a step further than what I am looking for.

Is there a well known method for writing and sharing proofs of mathematical statements that uses only mathematical symbols and is not a full blown programming language? And if not, why is this considered "taboo" or "informal"?

Thanks,

--jc

EDIT: I guess this turned out to not be a real question? Strange, I checked, it definitely ends in a question mark. Thanks everyone for the help, advice, and links. I appreciate your input.

-
Your fellow mathematicians are humans and not computers, and humans have an easier time reading words than symbols. – Qiaochu Yuan Feb 14 2011 at 22:23
So you want a language without the expressive power and the evocativeness of natural languages, yet also without the verifiability and objectivity of programming languages? Why? – darij grinberg Feb 14 2011 at 22:25
Part of the issue is that what you may think of as a "complex proof" and what a professional mathematician thinks of as a "complex proof" are two different things. (I think I can safely assume that you are an undergraduate). It is not unusual in mathematics to have proofs that are 100+ pages long in natural language, especially for the more foundational results. Translated in a more formal language, they would easily fill thousands of pages each. It is probably hard for you to imagine, but believe me, there would be no insight gained from this. [...] – Thierry Zell Feb 14 2011 at 23:09
Dear jc, I think that Thierry Zell's first comment above is perhaps the most relevant. Assuming that you are an undergraduate, and the logic and set theory course that you describe is one of the most advanced (in terms of proof writing and reading) courses that you have taken, your experience with what is a complex argument, and the best ways to think about it, are limited in comparison to the experiences of professional mathematicians. I don't say this to be critical: indeed, there is some value in transcribing written English proofs into formal symbols (and also going back the other way), – Emerton Feb 15 2011 at 5:52
... and if you find it helpful, there is no need not to keep doing it. Usually professional mathematicians understand proofs in a myriad of different ways, but the parts of the proof that can be readily formalized (or semi-formalized) into a "pure math" language of the type you envisage are often the easiest parts to understand. (With experience, aspects of proofs that seem very technical, or baroque, to beginners, become quite routine and straightforward.) What professionals want to focus on in any proof are the new ideas, the conceptual engines that make the argument run, and ideas are – Emerton Feb 15 2011 at 5:55
show 18 more comments

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.

-
Interesting. Has anyone tried using proof-checking software in teaching course on how to write proofs? – Michael Hardy Feb 15 2011 at 16:11
In Bonn, they have used Naproche in this way. I've heard that they have some computer labs sometimes full of students writing out semi-formal proofs into the system. – Joel David Hamkins Feb 15 2011 at 16:16
Fascinating. An obvious point that I would like to belabor, though, is that this seems a long way away from the transcription into pure symbols that was mentioned in the original question. – Thierry Zell Feb 15 2011 at 20:40
@Joel At first glance, this does not look like what I was hoping for. However, it does look like it is the closest thing to what I described that exists. It seems to me that it would be fairly straight forward to extend the parser to work with "pure symbols", although I don’t think that's what the authors have in mind when they say "controlled natural language." Thank you for taking the time to write up your response, I am marking it as the answer since it seems likely that this system is as close to what I am looking for as I am going to get. Thanks again, --jc – jc Feb 15 2011 at 22:55
@Thierry, jc -- unless I misunderstand, this is not a long way away from a formal language. It is instead, an interpreter away from a formal language. And that interpreter has been written. So the combination is a precise answer to the original question. – Sam Nead Feb 16 2011 at 17:21

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.

-
Very subtle way of asking to be included in the colourful language list! :) – Mariano Suárez-Alvarez Feb 15 2011 at 16:42

Perhaps this item is relevant: http://www.ams.org/notices/200811/tx081101370p.pdf

And another item: Lamport's "structured proofs": http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf

-
I replaced the link filled with Google-crud by the actual link to the article. – David Roberts Feb 14 2011 at 23:56
Thanks, this was very helpful. – jc Feb 15 2011 at 3:55

I suggest you take a look at the site of Freek Wiedijk:

http://www.cs.ru.nl/~freek/

He is a lot of papers about different formalizations. Also, some talks about 'proof sketches'. Set theory, is not the only formalization.

Also take a look at HOL light:

http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html

This formal logic, but not set theory, it is typed lambda calculus. It may inspire you for other ways of formalization than set theory.

Lucas

-
 Thanks, this looks like a lot to digest, but very interesting. – jc Feb 15 2011 at 3:55

(I accidentally posted this as an answer to a different question - gulp! Not paying attention)

From this article in the Notices of the AMS, we have an excerpt from Paul Halmos:

My advice about the use of words can be summed up as follows. (1) Avoid technical terms, and especially the creation of new ones, whenever possible. (2) Think hard about the new ones that you must create; consult Roget; and make them as appropriate as possible. (3) Use the old ones correctly and consistently, but with a minimum of obtrusive pedantry. [...]

Everything said about words, applies, mutatis mutandis, to the even smaller units of mathematical writing, the mathematical symbols. The best notation is no notation; whenever possible to avoid the use of a complicated alphabetic apparatus, avoid it. A good attitude to the preparation of written mathematical exposition is to pretend that it is spoken. Pretend that you are explaining the subject to a friend on a long walk in the woods, with no paper available; fall back on symbolism only when it is really necessary.

-

I think Funmath might be exactly what you are looking for.

-
 Looks very interesting, but the link was dead (I had to use google's cache at webcache.googleusercontent.com/… ) – Kevin O'Bryant Feb 26 2011 at 21:07 @Kevin: I've fixed the broken link. – Russell O'Connor Mar 4 2011 at 17:03

you can see an example of semi formal proof in:

http://www.testingexperience.com/testingexperience15_09_11.pdf

-