Pretty much this. I designed my own research harness and infra for theorem proving and conjecturing; however, you still need to review formulations!