I have some experience with both the situation posed by the question and Matt Noonan's modification in the comments.
Note taking in seminars: At a recent conference, I took notes directly on to my computer using a graphics tablet in conjunction with the program xournal. I have gotten a little frustrated in the past at having stacks of notes from seminars that are virtually useless to me because I'm rubbish at organising them and finding them again. The main benefit of writing them directly on to my computer was that I could then add the files to my reference database (refbase) where I could store the meta-data in searchable form. To emphasise that point, it is the meta-data that is searchable, not the information from the original talk.
I found a few other side-benefits from this method. I was slightly faster in writing on a graphics tablet than on paper; I think that that is to do with a different posture and the fact that to go from looking at the computer screen to looking at the board is quicker than going from hunched over paper to looking at a board. This might not be the same for something like a digital pen, though. I think I was also faster because I was less bothered about what my notes looked like - when writing on real paper, I try not to waste paper so if the lecture is getting near the end, I'll cram the last bit on the small bit left of the current page rather than start a new one; on the computer, I just make the page bigger. It's also easier to correct things, and to add more space in the middle of something already written (when the lecturer goes back and adds yet more symbols to the diagram!).
The only drawback at that conference was when my computer ran out of battery power 5 minutes before the end of the seminar and I lost the whole lot because the program didn't have an auto-save feature! (I wrote one that evening - isn't open source wonderful! - but I see now that the latest version of xournal as auto-save anyway).
Another drawback is simply the amount of desk space that this system takes up. I couldn't do this at another recent conference because it was in one of those auditoria where there is a tiny side desk which forces you to write on postage stamps.
I did think of trying to combine LaTeXing seminar notes with a graphics tablet: the idea being to have a LaTeX document in to which you type the majority of the notes, but then overlay diagrams (or other annotations) with the pen. While I think that this would be feasible, the software needs a little tweaking for all of this to work seamlessly.
Incidentally, decent graphics tablets are extremely cheap (I got mine for about 35 quid), and it doesn't take much to get used to writing on a different place to where the text appears, so if you're not sure but think it's something you'd like to try, I'd recommend a simple graphics tablet over getting something more expensive in the first instance. Also, a graphics tablet is great if you want to put fancy animations in your talks.
Giving Seminars/Lectures Using a Beamer+Pen: I'm now in the course of my second course doing this. I prepare the lectures using LaTeX+beamer but when I give them then I have a graphics tablet to hand to make annotations as necessary. Sometimes I leave whole problems to be "done live" - by the students, that is. The first time through, I used my graphics tablet and xournal. This time, the lecture hall that I'm in has a PC with a "write-on screen". Unfortunately, it runs Windows but fortunately, there's jarnal. There is a "new page" facility which brings up a blank slide on which you can write whatsoever you like. After the lecture, I put the annotations on the web page for the students.
I should say that there are several reasons that I've switched from chalk to presentations for lecturing.
I give better lectures/seminars when I use a computer than when I use chalk. This is (I think) because it forces me to prepare the whole seminar/lecture properly in advance and not think "I know how to do that" without carefully checking that I really do.
Chalk dust irritates my skin.
I teach in English but my students listen in Norwegian. If I gave the traditional "copy down everything I write on the board" lecture then the lag time while I waited for them to copy stuff down would be too great (I mean that the time that I assign for the students to catch up with copying down and be ready to listen to me again is significantly longer because they are reading, writing, and hearing in a non-native language). So I make the notes available in advance so that they have a baseline of what I'm going to say and can add to it as they feel the need.
I can actually look at the students and see their reactions while I'm lecturing instead of spending half the time looking at the board. That means that I can be far more reactive in what I'm actually saying.
The main drawback is the increased preparation time. But, due to 1, I'm not sure how much of that is because it forces me to prepare properly and how much is due to the nature of the preparation. An additional benefit will be that I have much less preparation to do next time I teach those courses (I say "will" because I've yet to repeat one of these courses. Perhaps I should say "hope").
You can see what it all looks like by looking at the course webpages for these two courses, they are here for the completed course and here for the current course.
Note: I have lots of macros that interact nicely with beamer and make life considerably easier for myself. I also ended up hacking xournal a little to make it better for note-taking. Same again for refbase to make it suitable for mathematicians (it was written by geologists). I'm happy to share any of these modifications, of course.
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.
Best Answer
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
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.