Bourbaki Proof Checker [pdf]

web.archive.org

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.

Reply on news.ycombinator.com