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 ; 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 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