Or it means accepting that your prover will need occasional hints from a human expert. I think this will always be true, when we're doing software verification

Or it means accepting that your prover will need occasional hints from a human expert. I think this will always be true, when we're doing software verification. Another way to look at the problem, then, is: how do we reduce the need for manual intervention to a minimum?