my emacs language workbench almost has a proof assistant! it’s J-Bob, the simple proof assistant from The Little Prover that they derived from the core of ACL2
it’s solving proofs! but for some reason I have to eval the result for it to finish, which is bizarre
the language itself is a very restricted namespace implemented on top of the elisp readtable reader. one day once I have better namespaces, this probably deserves to be reimplemented on top of that