From a proof-theoretic point of view, Lamport essentially suggests is writing proofs in natural deduction style, along with a system of conventions to structure proofs by the relevant level of detail. (It would be very interesting to study how to formalize this kind of convention -- it's something common in mathematical practice missing from proof theory.)
I have written proofs in this style, and once taught it to students. I find that this system -- or indeed any variant of natural deduction -- is extremely valuable for teaching proof to students, because it associates to each logical connective the exact mathematical language needed to use it and to construct it. This is particularly helpful when you are teaching students how to manipulate quantifiers, and how to use the axiom of induction.
When doing proofs myself, I find that this kind of structured proof works fantastically well, except when working with quotients -- i.e., modulo an equivalence relation. The reason for this is that the natural deduction rules for quotient types are rather awkward. Introducing elements of a set modulo an equivalence relation is quite natural:
$$
\frac{\Gamma \vdash e \in A \qquad R \;\mathrm{equivalence\;relation}}
{\Gamma \vdash [e]_R \in A/R}
$$
That is, we just need to produce an element of $A$, and then say we're talking about the equivalence class of which it is a member.
But using this fact is rather painful:
$$
\frac{\Gamma \vdash e \in A/R \qquad \Gamma, x\in A \vdash t \in B \qquad \Gamma \vdash \forall y,z:A, (y,z) \in R.\;t[y/x] = t[z/x]}{\Gamma \vdash \mbox{choose}\;[x]_R\;\mbox{from}\;e\;\mbox{in}\;t \in B}
$$
This rule says that if you know that
- $e$ is an element of $A/R$, and
- $t$ is some element of $B$ with a free variable $x$ in set $A$, and
- if you can show that for any $x$ and $y$ in $R$, that $t(y) = t(z)$ (ie, $t$ doesn't distinguish between elements of the same equivalence class)
Then you can form an element of $B$ by picking an element of the equivalence class and substituting it for $x$. (This works because $t$ doesn't care about the specific choice of representative.)
What makes this rule so ungainly is the equality premise -- it requires proving something about the whole subderivation which uses the member of the quotient set. It's so painful that I tend to avoid structured proofs when working with quotients, even though this is when I need them the most (since it's so easy to forget to work mod the equivalence relation in one little corner of the proof).
I would pay money for a better elimination rule for quotients, and I'm not sure I mean this as a figure of speech, either.
I have given talks about mathematics to non-mathematicians, for example to a bunch of marketing people. Supplemental: to see an example of a talk of mine that was given to a general audience, see my TEDx talk "Zeroes" (with supplemental material). The talk lasted 15 minutes and it took me about two weeks to prepare.
In my experience the following points are worth noting:
- If the audience does not understand you it is all in vain.
- You should interact with your audience. Ask them questions, talk to them. A lecture is a boring thing.
- Pick one thing and explain it well. The audience will understand that in 10 minutes you cannot explain all of math. The audience will not like you if you rush through a number of things and you don't explain any one of them well. So an introductory sentence of the form "Math is a vast area with many uses, but in these 10 minutes let me show you just one cool idea that mathematicians have come up." is perfectly ok.
- A proof of something that seems obvious does not appeal to people. For example, the proof of Kepler's conjecture about sphere packing is a bad example because most people won't see what the fuss is all about. So Kepler's conjecture would be a bad example.
- You are not talking to mathematicians. You are not allowed to have definitions, theorems or proofs. You are not allowed to compute anything.
- Pictures are your friend. Use lots of pictures whenever possible.
- You need not talk about your own work, but pick something you know well.
- Do not pick examples that always appear in popular science (Fermat's Last Theorem, the Kepler conjecture, the bridges of Koenigsberg, any of the 1 million dollar problems). Pick something interesting but not widely known.
Here are some ideas I used in the past. I started with a story or an intriguing idea, and ended by explaining which branch of mathematics deals with such ideas. Do not start by saying things like "an important branch of mathematics is geometry, let me show you why". Geometry is obviously not important since all of mathematics has zero importance for your audience. But they like cool ideas. So let them know that math is about cool ideas.
To explain what topology and modern geometry are about, you can talk about the Lebesgue covering dimension. Our universe is three-dimensional. But how can we find this out? Suppose you wake up in the morning and say "what's the dimension of the universe today?" You walk into your bathroom and look at the tiles. There is a point where three of them meet and you say to yourself "yup, the universe is still three-dimensional". Find some tiles in the classroom and show people how always at least three of them meet. Talk about how four of them could also meet, but at least three of them will always meet in a point. In a different universe, say in a plane, the tiles would really be segments and so only two of them would meet. Draw this on a board. Show slides of honeycombs in which three honeycomb cells meet. Show roof tilings in which thee tiles meet, etc. Ask the audience to imagine what happens in four dimensions: what do floor tiles in a bathroom look like there? They must be like our bricks. What is a chunk of space for us is just a wall for them. So if we have a big pile of bricks stacked together, how many will meet at a point? At least four (this will require some help from you)!
To explain knot theory, start by stating that we live in a three-dimensional space because otherwise we could not tie the shoelaces. It is a theorem of topology that knots only exist in three dimensions. You proceed as follows. First you explain that in one or two dimensions you can't make a knot because the shoelace can't cross itself. It can only be a circle. In three dimensions you can have a knot, obviously. In four dimensions every knot can be untied as follows. Imagine the that the fourth dimension is the color of the rope. If two points of the rope are of different color they can cross each other. That is not cheating because in the fourth dimension (color) they're different. So take a knot and color it with the colors of the rainbow so that each point is a different color. Now you can untie the knot simply by pulling it apart in any which way. Crossing points will always be of different colors. Show pictures of knots. Show pictures of knots colored in the color of the rainbow.
Explain infinity in terms of ordinal numbers (cardinals are no good for explaining infinity because people can't imagine $\aleph_1$ and $2^{\aleph_0}$). An ordinal number is like a queue of people who are waiting at a counter (pick an example that everyone hates, in Slovenia this might be a long queue at the local state office). A really, really long queue contains infinitely many people. We can imagine that an infinite queue 1, 2, 3, 4, ... is processed only after the world ends. Discuss the following question: suppose there are already infinitely many people waiting and one more person arrives. Is the queue longer? Some will say yes, some will say no. Then say that an infinite row of the form 1, 2, 3, 4, ... with one extra person at the end is like waiting until the end of the world, and then one more day after that. Now more people will agree that the extra person really does make the queue longer. At this point you can introduce $\omega$ as an ordinal and say that $\omega + 1$ is larger than $\omega$. Invite the audience to invent longer queues. As they do, write down the corresponding ordinals. They will invent $\omega + n$, possibly $\omega + \omega$. Someone will invent $\omega + \omega + \omega + \ldots$, you say this is a bit imprecise and suggest that we write $\omega \cdot \omega$ instead. You are at $\omega^2$. Go on as far as your audience can take it (usually somewhere below $\epsilon_0$). Pictures: embed countable ordinals on the real line to show infinite queues of infinite queues of infinite queues...
Best Answer
What I noticed is that the infamous question "so what?", though seldomly asked directly, can be read in the eyes of the audience every time when the following three (rather common) conditions are satisfied:
a) there is nobody in the audience who ever thought of the question himself
b) there is no catchy picture or phrase in the presentation
c) some non-zero special knowledge is needed to understand even the statement of the theorem.
It doesn't really matter much what kind of result is being presented: a non-existence one, or something else though condition (b) (the only one you really have some control over during the talk) is much harder to violate when you are presenting a non-existence theorem. Indeed, you, apparently, cannot provide a fascinating example of an entity that doesn't exist in mathematics. Neither cannot you conclude with "we still do not understand a lot about the behavior of this fascinating object" when the object does not exist. And the whole thing often looks about as exciting as a report of a treasure hunting expedition that ends up with "so, after spending many days questioning the locals, climbing, digging, etc., we can safely conclude that there has never been anything of value in that area".
Still, one can be impressed with a pure impossibility theorem.
My favorite non-existence result is the impossibility to find an elementary antiderivative of $\frac{e^x}{x}$. It is useless to try to impress a layman with it. The appreciation I have comes from the fact that in my case (a) and (c) were violated.
First, when I was a student our calculus recitation sections consisted for one semester almost exclusively of finding some tricky antiderivatives. Many of those were of the kind where changing a single sign or a coefficient would result in an unsolvable problem and there were some misprints in the assignments. That made me wonder whether it might be possible to solve the problem as given. Of course, our teachers claimed that $\int \sin(x^2)dx$ and such cannot be presented by a neat formula but they never gave us even the slightest hint why. We saw, of course, that no standard integration trick worked but that might merely mean that there are some new tricks to discover. I was smart enough not to try what was claimed to be proven impossible but not smart enough to prove that impossibility or even to have a decent idea about how such things could be proved in general. I thought of asking my teachers about it but I suspected (rightly, as it turned out) that they knew it no better than I and no analysis textbook I was reading gave me the slightest clue.
That was in Russia back in 80's, so you could not just google "Liouville theorem" up or download any fancy book you wanted from the web. So, I remained completely ignorant until much later, when I was a postdoc at MSU, I visited the University of Toledo and met Rao Nagissetti who gave me some papers of his. To my great surprise, those were about impossibility to solve some quadratic differential equations in elementary functions. The old memories returned at once and I read those papers overnight. The ideas were completely novel to me though I have read Lang's algebra by then and wasn't afraid of Galois theory and such; I just viewed all that as something infinitely remote from any analysis question. That was one of the few times in my life when I was genuinely impressed: the proof lay not beyond my technical abilities (it isn't technically difficult at all) but beyond the range my imagination.
I leave it to you to derive a moral from this story (if it has any). I want only to say that I have managed to forget many things I learned but I doubt I'll ever forget the Liouville theorem. I played with it a bit too over the years (See http://www.artofproblemsolving.com/Forum/viewtopic.php?p=2471315#p2471315 for my latest attempt. It also shows that today some kids are as curious about these questions as I was 25 years ago).