[FOM] Talk on Formal Verification

[Walt Read]

> It is paradoxical that, on the one hand, many such efforts have been wildly successful, but on the other hand, they show no signs of any capability in regard to the sort of insights we have been discussing on this list. ... The situation is reminiscent of computer chess, where on the one hand, a computer program can beat the world champion, but on the other hand, no chess-playing program can explain why a given move is good or bad, or compare two positions to state whether an idea that works in one would be likely to work in the other.
>
> Larry Paulson
>

Which of course goes to the question of what we mean by getting
insights or understanding from AI results. What are we expecting when
we look for "understanding" or "insight"? Does "everything is a set"
constitute an advance in understanding what's going on in a lot of
math? Or the development of abstract algebraic structures? In some
ways these seem like generalizations that an AI program might get.
Maybe heuristics like "look at the remainders on division by n and use
the pigeon-hole principle"? Are insights essentially good heuristics
that say "look here rather than there; you're apt to get to the result
quicker"? (Even chess programs have heuristics like "control the
center" and "protect the king". It's not all grind.) And if a program
is ever going to be able to communicate its insights to us, if that
even makes any sense, it will have to speak our language. If the
computer works in numbers, it will have to explain in numbers. ("...
because my evaluation function gave this a 1294 and that only a 1168")
If we expect it to say "because this gives me control of the KB file"
or "it's actually just a fixed-point theorem", then it will have to be
able to work with problems in those terms. These issues of language or
representation are central.

It would be useful to have some concrete examples from math of proofs
that gave (you individually, the math community) some real insight or
understanding.

-Walt