From lusk Sat Jun 18 09:10:25 1994 Received: from linus.mitre.org (linus.mitre.org [129.83.10.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id JAA11902 for ; Sat, 18 Jun 1994 09:10:03 -0500 Received: from localhost (localhost [127.0.0.1]) by linus.mitre.org (8.6.7/RCF-6S) with ESMTP id KAA19441 for ; Sat, 18 Jun 1994 10:10:01 -0400 Message-Id: <199406181410.KAA19441@linus.mitre.org> To: qed@mcs.anl.gov Subject: Re: Examples In-reply-to: Your message of "Fri, 17 Jun 1994 22:31:07 MDT." <94Jun17.223123-0600.18656-1@scapa.cs.ualberta.ca> Date: Sat, 18 Jun 1994 10:09:59 -0400 From: "F. Javier Thayer" >> Could you suggest something? I'm not sure what the question is, but I assume you want me to suggest something that is possible to do from the existing Mizar library of theorems. Wouldn't a development of the first few chapters of Dieudonne's book "Foundations of Modern Analysis be" a possibility? I also think Victor Yodaiken's suggestion of "Concrete Mathematics" is an ambitious, but in my opinion feasible project using any of the currently existing theorem checkers/provers. THAT would be real eye catcher don't you think? Javier Thayer