Logic List Mailing Archive

Automath symposium; Eindhoven (May 2004)

We are happy to announce the following short symposium on the occasion of
the digitization of a large part of the Automath Archive. The symposium is
organized in a cooperation of the ZIC-colloquium with the Brouwer seminar
of the Foundations group in Nijmegen. We would like to apologize to those
who receive multiple copies of this invitation.

                          AUTOMATH Symposium

                   A workshop on the occasion of the
                 digitalizing of the Automath Archive

                     Wednesday 26 May 2004,
                      Eindhoven University,
                          Auditorium 16
                         14:30 - 17:30h


Can computers help us with proofs?

Recently, a proof has been published on the most efficient way to stack
oranges, a problem pending since the times of Johannes Kepler. However, an
important part of this proof, given by the American mathematician Thomas
C. Hales, hinges on a complex computer calculation -- as was the case with
the well-known Haken-Appel solution of the four-colour theorem, in 1976.

An important question is whether computer assisted proofs are acceptable
to the scientific community. One can distinguish romantic (human
understandable)  vs cool (machine verified) proofs. The heart of the
matter is whether a proof is reliable.  Reliability can be obtained by
providing fully formalised proofs that can be algorithmically verified.
The methodology of de Bruin's Automath Project delivers proofs that are
reliable and human-readable.

What is the feasibility of constructing fully formalised proofs for
`everyday use' in mathematics? Interactive support from the computer in
developing proofs brings us a step forward, but how far can we get?


On these matters a short symposium is organised, collectively by the
Universities of Nijmegen and Eindhoven. The speakers are the recent
Spinoza-prize winner Henk Barendregt, Herman Geuvers and Freek Wiedijk.
They will give short presentations on the subject.

In connection with the talks there will be a festive homage to professor
N.G. de Bruijn, famous pioneer in the field of computer proving. The
occasion is that a whole collection of early papers on his Automath
project, dating from the sixties and seventies, has now been
electronically archived, thus making them publicly available.  The web
version of the digitalized archive is already online at the dedicated
Automath Archive site (http://automath.webhop.net/) developed by Mark

In a final talk, professor de Bruijn intends to give his views on the
value of computer proofs.



The symposium is scheduled on
Wednesday May 26th, 14.30 - 17.30 hrs,
at Technische Universiteit Eindhoven, Auditorium, Room 16.

14:30 - 14:50 Coffee and Tea
14:50 - 15:10 Henk Barendregt
15:10 - 15:30 Herman Geuvers
15:30 - 15:50 Freek Wiedijk
15:50 - 16:10 Break
16:10 - 16:20 Presenting the Automath Digital Archive to prof. de Bruijn
16:20 - 16:40 prof. de Bruijn
16:40 - 17:30 Reception


Titles and abstracts of the talks:
Title: Automath: challenges and ideals
Speakers: Henk Barendregt, Freek Wiedijk, Herman Geuvers

Abstract: The basic idea behind Automath was to develop a "justification
system"  (as De Bruijn calls it in his 1991 overview article). Since the
start of Automath there have been many efforts to reach goals similar to
Automath: many "justification systems" have been defined, implemented and
tested on real mathematical examples.  We give an overview of the goals of
Automath and its heritage and we try to find out where we stand in the
development of an ideal justification system and which challenges lie


This is a joint meeting of the The Foundations Group / Brouwer Institute
Seminar (Nijmegen) and the ZIC Colloquium (Eindhoven).

Any additional information will be announced at the webpage of the

For more information, please contact:

Francien Dechesne
or Georgi Jojgov