Bourbaki Proof Checker [pdf] (web.archive.org)

1 comment

[ 1.7 ms ] story [ 10.1 ms ] thread

Metamath style but implemented in lisp. The idea is one can write lisp functions that define theorems, analogous to using SML to define theorems in Edinburgh LCF.