3 ms·Bourbaki Proof Checker [pdf]1 points by JonChesterfield 3y agoJonChesterfield 3y agoMetamath 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.