[FOM] Talk on Formal Verification
Timothy Y. Chow
tchow at alum.mit.edu
Sat Feb 6 13:58:39 EST 2016
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"
> 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.
More information about the FOM