There are some automated theorem provers for higher-order logic [0][1], but they are not very good yet compared to their first-order counterpart. There are also

There are some automated theorem provers for higher-order logic [0][1], but they are not very good yet compared to their first-order counterpart. There are also some provers specialized in inductive proofs [2][3], although the frontier with proof assistants such as Coq or Isabelle starts getting blurry as you often need the user's intervention to explicitely provide lemmas. I have some hopes that this is going to change in the next few years thanks to a colleague's effort [4] to build better higher-order provers. He's an expert in Sledgehammer (a tool to use automated provers from Isabelle) which is already a productivity boost, and should become better with this project. You are right that the search space is more difficult to handle. Induction (and similar formulas) is particularly hard to handle because one usually has to introduce lemmas, and these lemmas have to be "guessed" (infinite branching factor there). Existing provers basically rely on heuristics to try and find lemmas that would be useful for solving the current goal(s). ACL2 [3] for instance uses heuristics accumulated and refined for decades. Hopefully, proof assistants will get tighter and tighter integration with automated provers, and the user will have to specify only the main lemmas and the overall shape of a proof, leaving the details to CPU crunching. [0] https://page.mi.fu-berlin.de/cbenzmueller/leo/ https://page.mi.fu-berlin.de/cbenzmueller/leo/ [1] https://www.ps.uni-saarland.de/~cebrown/satallax/ https://www.ps.uni-saarland.de/~cebrown/satallax/ [2] https://github.com/sorinica/spike-prover https://github.com/sorinica/spike-prover [3] https://www.cs.utexas.edu/users/moore/acl2/ https://www.cs.utexas.edu/users/moore/acl2/ [4] http://matryoshka.gforge.inria.fr/ http://matryoshka.gforge.inria.fr/