Re: A question

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

In my question posted a few days ago I was asking for information
about formalization of any substantial chunk of mathematics formally
checked but I never defined what such a chunk is.  I indicated that I
was most interested in books or parts of books that were originally
meant for human consumption.

I got quite a number of answers for which I would like to thank.  Most
of the answers concerned relatively isolated developments even if they
covered advanced material.  Of the books or part of books having the
nature of mathematical monographs that were formalized I have only the
following:

	- In the 1970's L. S. Jutting formalized Landau's {\em Grundlagen
	  der Analysis} in de Bruijn's AUTOMATH system.  The same material
	  was then covered by Udding in a way directly written for Automath.

	- D. L. Simon in his 1990 PhD thesis at University of Texas at Austin
          checked {\em The elementary theory of numbers} by Leveque using 
          the Boyer-Moore prover.

	- J. Siekmann's group from Saarbr\"{u}cken started checking
          D\"{u}ssen's {\em Halbgruppen und Automaten} in the MKRP prover 
          in the 1980's.

	- Shang-Ching Chou: Mechanical Geometry Theorem Proving,
          D. Reidel Publishing Company, 1987 supposedly tries to formalise 
          Euklid's Elements but I could not lay my hands on the book yet.

        - L.~C.~Paulson and K.~Gr\c{a}bczewski reported on the Isabelle 
          formalization of most of Chapter I of Kunen's {\em Set Theory} 
          and two first chapters of Rubin and Rubin, {\em Equivalents of 
          the Axiom of Choice}.

        - T. Nipkow formalized in Isabelle/HOL the first 100 pages of 
          Winskel's {\em The Formal Semantics of Programming Languages}.

	- Compendium of continuous lattices in Mizar.

I am also aware of some formalizations under way in Nijmegen.  

I am sure that there are more efforts of the kind I am looking for, so should
you know another one, please let me know.

Thanks,

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr