[l2h] Structured Proofs

[George Leibman]

This is a multi-part message in MIME format.
--------------F24154E5F6DF3F0643859061
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit

Hi,
A few years ago, Leslie Lamport (yes, the Godfather of LaTeX) proposed,
in an article in the American
Mathematical Monthly, a way of writing a mathematical proof in a
recursive style with required facts
used in the proof themselves proven in the same format, and so on.  He
even suggested that a hyperlink
system would be the preferred presentation technology, as the deeper
details of a proof could remain hidden
until requested by the user by clicking on a fact to see its proof.

As a moderately computer-literate student of mathematics, I am wondering
if anyone has implemented
such a system as an enhancement to latex2html.  I am contemplating doing
this, but I would be just as
happy to learn that such a working system is already available.

Has anyone implemented or seen anything like this?

--
George Leibman
100 Diplomat Drive, Apt. 6F
Mount Kisco, NY 10549

(914)241-2723
gleibman@acedsl.com



--------------F24154E5F6DF3F0643859061
Content-Type: text/x-vcard; charset=us-ascii;
 name="gleibman.vcf"
Content-Transfer-Encoding: 7bit
Content-Description: Card for George Leibman
Content-Disposition: attachment;
 filename="gleibman.vcf"

begin:vcard 
n:Leibman;George
tel;cell:(914)589-5723
tel;fax:(212)706-3100
tel;home:(914)241-2723
tel;work:(212)706-3254
x-mozilla-html:FALSE
adr:;;100 Diplomat Drive Apt 6F;Mount Kisco;NY;10549;USA
version:2.1
email;internet:gleibman@acedsl.com
x-mozilla-cpt:;0
fn:George Leibman
end:vcard

--------------F24154E5F6DF3F0643859061--