# [FOM] Talk on Formal Verification

Louis Garde louis.garde at free.fr
Sat Feb 6 00:54:07 EST 2016

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

```