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)

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.



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.

See also