[FOM] Talk on Formal Verification

[Louis Garde]

Le 05/02/2016 21:42, Walt Read a écrit :
> These techniques can work well for board games and other situations
> where we only have to find a specific path along a well-defined tree.
> But in getting new results in math, there's no fixed list of legal
> moves.
If there were no fixed list of legal moves, computers would not be able 
to verify a formalized proof either.
Within a given formalized theory, there is always a fixed list of legal 
moves. Or the theory is not fully formalized.
There is no reason that AI is not able to find new formalized proofs in 
a given formalized theory.

Le 05/02/2016 23:02, Timothy Y. Chow a écrit :
> In fact I think there's a good chance that if computers eventually 
> become better than humans at doing mathematical research, a byproduct 
> will be that we'll become convinced that mathematical research doesn't 
> require creativity or insight.
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.
If the proof is obtained by "gluing together" a list of known 
reasonings, then the computer could be able to output the used 
reasonings, in a human-understandable way (if not too long).
Possible, but not easy: it is already a big challenge for Formal 
Verification to find a way to write human-understandable formalized proofs !

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...

For instance, having the chess or go computer programs being able to 
beat human champions is (was) the first step.
The second step would be to have the chess or go computer programs being 
able to show, in a human-understandable way, the known tactics that were 
applied to beat the champion (if any).
The next step would be to have the chess or go computer programs being 
able to explain, in a human-understandable way, some new tactics to beat 
the champions...

The way to reach a goal is usually more interesting than the goal 
itself. This is were creativity is required.
I don't think that AI will ever be able of such a human-understandable 
creativity. AI will for sure overpass human brain in many ways, but 
probably we will always be on our own to improve our understanding of 
mathematics: mathematical research will always remain of interest.

Louis.