For and on behalf of any genuine non-mathematicians, a couple of questions: (1) what would have to be the case such that his latest advances in proof assistance would not live up to his expectations (2) what things outside the world of abstract mathematics (such as in, but not restricted to the world of software) would change (such that anyone outside the field would notice) if they did live up to his expectations?