[FOM] Talk on Formal Verification

[Timothy Y. Chow]

Louis Garde wrote:
> I don't think so. I am convinced that one day computers will be able to 
> find new mathematical results, but it is then likely that the proof 
> cannot be understood by a human.

On this point you and I agree.

> But if the computer uses a different approach, it will give you a
> result, but no reasoning. You will have a proof, but not a "beautiful"
> proof.
> Creativity is required to give you a result with a reasoning, so that
> the reasoning (and not only the result) can be applied on a similar, but
> different, problem.
> The next step would be to have AI being able to build new reasonings
> that can be understood by a human...

My belief is that there will be two kinds of computer proofs:

1. those for which a humanly intelligible explanation does not exist; and

2. those for which a humanly intelligible explanation does exist.

In case 1, I don't think we can fault the AI for failing to come up with a 
humanly intelligible explanation.

In case 2, I doubt that "creativity" is really required.  I can imagine 
having a computer read a large corpus of texts in which humans try to 
explain things to other humans, and eventually figuring out how to 
generate "explanatory texts" that give humans a warm fuzzy feeling of 
understanding.  The computer won't have to be creative or even 
"understand" what it's saying.  It will just have to be good at producing 
natural-language texts that, when read by humans, make them feel that they 
understand what's going on.

Tim