HomePage RecentChanges

Formal maths bibliography

QED
an apparently defunct math archiving project with some striking similarities to the HDM, but with a greater emphasis on formality. A full critique/comparison would be nice to see.
A comparison of Mizar and Isar
by Wenzel and Wiedijk. The bibliography and the Related Work work subsection in the intro may be useful for survey and literature search purposes.
Abstract. In this paper we compare Mizar and Isar. A small example, Euclid's proof of the existence of infinitely many primes, is shown in both systems. We also include slightly higher-level views of formal proof sketches. Moreover a list of differences between Mizar and Isar is presented, highlighting the strengths of both systems from the perspective of end-users. Finally, we point out some key differences of the internal mechanisms of structured proof processing in either system.
Comparing mathematical provers
by Freek Wiedijk. A nice summary of the currently available engines and projects.
Abstract. We compare fiffteen systems for the formalizations of math- ematics with the computer. We present several tables that list various properties of these programs. The three main dimensions on which we compare these systems are: the size of their library, the strength of their logic and their level of automation.
The foundation of a generic theorem prover
by L. Paulson. A useful resource for learning about theoretical aspects of formal maths. Discusses meta-logic, higher order logics, inference, and the LCF deduction system. More of Paulson's papers are available here
Abstract. Isabelle is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or `logical framework') in which the object-logics are formalized.

I happened to stop in at Barnes and Noble yesterday and I spotted a new paperback called "Meta Math!" by Gregory Chaitin. I didn't buy it (I was already buying Minsky's new book and a paperback copy of Adams's Long Dark Teatime and couldn't justify the further $14 expense without checking at my local library first) but I can certainly recommend it. Chaitin uses a wide-gauge topic-filter, so, about half the book is about his thoughts about philosophy and his personal life and like that, whereas the other half is mathematics and metamathematics and Lisp and such. I figure people around here are into that sort of mixture, so I'll pass along the recommendation. --jcorneli