LCF style proof assistant A minimal propositional logic proof assistant Features hundred_monkeys tactic, can a hundred monkeys prove your theorem, find out! monkeys_tac tactic, when a hundred monkeys are not enough auto the monkeys fought back so we implemented auto