Notes from the Logbook of a Proof-Checker’s Project*

Abstract

We present three newsletters drawn from the documentation of a project aimed at developing a software system which ingests proofs formalized within Zermelo-Fraenkel set theory and checks their compliance with mathematical rigor. Our verifier will accept trivial steps as obvious and will be able to process large proof scripts (say dozens of thousands of proofware lines written on persistent files). To test our prototype proof-checker we are developing, starting from the bare rudiments of set theory, various “proof scenarios,” the largest of which concerns the Cauchy Integral Theorem.

The first newsletter is devoted to the treatment of inductive sets and to the issue of proof modularization, in sight of possible applications of our computerized proof environment in program correctness verification. The second newsletter proposes a decision procedure for ordered Abelian groups, examined in detail, as a candidate for inclusion in the inferential core of our verification system.

The third newsletter discusses how to best define the set of real numbers and prove their basic properties. After having experienced difficulties with the classical approach devised by Dedekind, we now incline to follow the approach originally developed by Cantor and recently adapted by E. A. Bishop and D. S. Bridges.

Work partially supported by MURST/MIUR Grant prot. 2001017741 under project “Aggregate- and number-reasoning for computing: from decision algorithms to constraint programming with multisets, sets, and maps.”