# A question (sorry if repeated)

Hi:

On April 25 I posted the following question to qed@mcs.anl.gov:

Grzegorz Bancerek and I are writing a sort of half-way report
on the formalization of "A Compendium of Continuous Lattices" in Mizar.
Another effort that (I am aware of) of formalizing an entire book
is Jutting's formalization of Landau's "Grundlagen der Analysis" in
AUTOMATH in the 70's.

Does anybody know about other efforts on formalizing an entire book?

To my surprise - the answer was that essentially "no".  The responses that
I got are summerised in the paragraph attached below.

I would like to repeat my question not asking necessarily for a
complete book anymore but any SUBSTANTIAL chunk of mathematics formally
checked.  Now, what is such a chunk?  Hard to say but it should be
foundational work, without assuming convenient facts when needed.
Books or parts of books would be best.

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

-------------------------

In the past, there were some attempts to formalize entire mathematical
books in computerized proof-checking systems.  The best known example
was done in the 1970's when L.~S.~Jutting formalized Landau's {\em
Grundlagen der Analysis} in de Bruijn's AUTOMATH system (see
~\cite{JUTTING,LANDAU,AUTOMATH}).  We are sure that in other proof
assistants, people have been undertaking similar efforts of
formalizing mathematical books, but we are aware of only two partially
completed attempts: 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, and in the 1980's, J.~Siekmann's
group from Saarbr\"{u}cken started checking D\"{u}ssen's {\em
Halbgruppen und Automaten} with the help of the MKRP prover.