[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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.

Thanks in advance,

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