From owner-qed Fri Nov 25 04:38:43 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id EAA10901 for qed-out; Fri, 25 Nov 1994 04:36:39 -0600
Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id EAA10894 for <qed@mcs.anl.gov>; Fri, 25 Nov 1994 04:36:32 -0600
Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Fri, 25 Nov 1994 10:36:04 +0000
To: qed@mcs.anl.gov
Subject: AUTOMATH
Date: Fri, 25 Nov 1994 10:35:55 +0000
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-ID: <"swan.cl.cam.:040030:941125103610"@cl.cam.ac.uk>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


I am looking for modern papers written in the tradition of Jutting's thesis,
Checking Landau's ``Grundlagen'' in the AUTOMATH System.  I mean papers that
take (part of) a mathematics book or paper, formalize the text as closely as
possible, and discuss statements/arguments that are hard to formalize.  

I know of a lot of mechanized mathematics in the literature, but little of the
sort described above.  Can anyone help?

							Larry Paulson