> Coq, Isabelle are interactive theorem provers or proof assistants, not automatic theorem provers which is a lot harder to do
Automatic theorem provers for first-order logic (FOL) have existed for some time [0], but higher-order logic (HOL) is another matter. The difference is that in HOL, predicates can be variables; in FOL they are all constants. HOL allows you to write rules for mathematical induction; for example:
∀P P(0) ∧ (∀n n ≥ 0 ∧ P(n) ⇒ P(n + 1)) ⇒ (∀n n ≥ 0 ⇒ P(n))
This says that for any predicate P on the natural numbers, if you can show, first, that P(0), and second, that for any natural n, P(n) implies P(n + 1), then you can conclude that P is true for any n. This rule is not a valid FOL statement, because it starts off quantifying over possible predicates, which is not permitted in FOL.
Reasoning of this kind, although usually informal, is necessary for programmers to understand any iterative or recursive piece of code. To understand such code, you have to know what invariant it maintains; proofs of such invariants are always inductive. So HOL is required, in most cases, for formal verification of software.
But no one has figured out how to build an automated prover for HOL. My own theory as to why is simply that the branching factor is higher. It's like the difference between chess and Go: the branching factor -- the average number of possible moves from any board position -- is small enough in chess that brute-force search can be sufficient to play at a world level, at least in the mid- and end-game; but in Go, it's much larger, so that brute-force search doesn't get you very far.
As you say, lacking a fully automated HOL prover, people have been using proof assistants instead. These keep track of the details of the proof, which is still a very useful function, and can perform certain simple deductive steps themselves, but require manual intervention at certain critical points, such as the introduction of induction hypotheses.
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.
Automatic theorem provers for first-order logic (FOL) have existed for some time [0], but higher-order logic (HOL) is another matter. The difference is that in HOL, predicates can be variables; in FOL they are all constants. HOL allows you to write rules for mathematical induction; for example:
This says that for any predicate P on the natural numbers, if you can show, first, that P(0), and second, that for any natural n, P(n) implies P(n + 1), then you can conclude that P is true for any n. This rule is not a valid FOL statement, because it starts off quantifying over possible predicates, which is not permitted in FOL.Reasoning of this kind, although usually informal, is necessary for programmers to understand any iterative or recursive piece of code. To understand such code, you have to know what invariant it maintains; proofs of such invariants are always inductive. So HOL is required, in most cases, for formal verification of software.
But no one has figured out how to build an automated prover for HOL. My own theory as to why is simply that the branching factor is higher. It's like the difference between chess and Go: the branching factor -- the average number of possible moves from any board position -- is small enough in chess that brute-force search can be sufficient to play at a world level, at least in the mid- and end-game; but in Go, it's much larger, so that brute-force search doesn't get you very far.
As you say, lacking a fully automated HOL prover, people have been using proof assistants instead. These keep track of the details of the proof, which is still a very useful function, and can perform certain simple deductive steps themselves, but require manual intervention at certain critical points, such as the introduction of induction hypotheses.
[0] https://en.wikipedia.org/wiki/Automated_theorem_proving