Bourbaki proof verifier

What is it?

Bourbaki is a system for writing and verifying formal mathematical proofs, written in Common Lisp.

Where can I get it?

Newest version (3.7) (2006-12-21)

Older versions:

3.6 (2005-12-10)
3.5
3.4

Getting started

> (load "init")
> (in-package bourbaki-user)
> (verify !!prop)

The theorem files are encoded in UTF-8 so you must set up a UTF-8 locale, for example:

$ LANG=en_EN.utf8 LC_ALL=en_EN.utf8 clisp

sbcl seems to have problems with memory usage when loading Bourbaki files. I recommend using clisp until this is sorted out.

Documentation

Version 3.7: <TeX> <PDF> (2006-12-21)
Version 3.6: <TeX> <PDF> (2006-02-15)
Version 3.5: <PDF>

Features

Sound definitions
Bourbaki files may contain arbitrary Lisp code for generating theorems, effectively serving as metatheorems.
Nested namespaces for theorems. For example: Set theory in !/set, Group theory in !/algebra!group. A lemma might be referred as !/algebra!group!thr!lemma1
Exporting theorems from different contexts. For example: if !/algebra!group contains theorems for arbitrary groups, one can do (export [!/algebra!group [R] [+]]) to get the theorems specialized to the additive group of real numbers.
Seeking theorems

What is included?

The Bourbaki library currently contains proposition calculus, predicate calculus with identity (mostly converted from Metamath) and the very beginnings of set theory. See the HTML output from an older version.