Danger(s) of theorem-proving AI? — LessWrong