For verified software, we probably don't need many big new theorems. We probably just need to be able to apply a large library of well-known strategies to a mi

For verified software, we probably don't need many big new theorems. We probably just need to be able to apply a large library of well-known strategies to a mind-numbingly long list of routine proof obligations. It's more about exhaustive case analysis, which computers are good at, than about creative leaps of intuition. The big problem, IMO, is search control: keeping the computer from wandering off into parts of the search space that don't actually matter.